Split development into two versions: with and without explicit substitutions and...
authorJoey Capper <jjc@cs.nott.ac.uk>
Tue, 22 May 2012 12:52:18 +0000 (13:52 +0100)
committerJoey Capper <jjc@cs.nott.ac.uk>
Tue, 22 May 2012 12:52:18 +0000 (13:52 +0100)
commit33d1afe854503d79aeed74e1f03937bae8932166
treecaf4e43169f43d071aa65093a4a07105e4123c4d
parentc687440cf299b9d275c9299f563778693d59f955
Split development into two versions: with and without explicit substitutions and correctness proofs.
Tentatively name TLDI and JFP, respectively.
41 files changed:
JFP/ContextMorphisms.agda [new file with mode: 0644]
JFP/Contexts.agda [new file with mode: 0644]
JFP/Equivalences.agda [new file with mode: 0644]
JFP/Examples.agda [new file with mode: 0644]
JFP/FHMExplicitSubst.agda [new file with mode: 0644]
JFP/Model.agda [new file with mode: 0644]
JFP/NormalForms.agda [new file with mode: 0644]
JFP/Reification.agda [new file with mode: 0644]
JFP/Soundness.agda [new file with mode: 0644]
JFP/Substitutions.agda [new file with mode: 0644]
JFP/Terms.agda [new file with mode: 0644]
JFP/Theorems.agda [new file with mode: 0644]
JFP/Types.agda [new file with mode: 0644]
JFP/Values.agda [new file with mode: 0644]
JFP/Variables.agda [new file with mode: 0644]
JFP/Weakening.agda [new file with mode: 0644]
TLDI/Contexts.agda [new file with mode: 0644]
TLDI/Convertibility.agda [new file with mode: 0644]
TLDI/Examples/BreakingPendulum.agda [new file with mode: 0644]
TLDI/Examples/Core.agda [new file with mode: 0644]
TLDI/Examples/Electrical.agda [new file with mode: 0644]
TLDI/Examples/Mechanics.agda [new file with mode: 0644]
TLDI/FHM.agda [new file with mode: 0644]
TLDI/FlatEquations.agda [new file with mode: 0644]
TLDI/Infer.agda [new file with mode: 0644]
TLDI/Labeling.agda [new file with mode: 0644]
TLDI/Normalisation.agda [new file with mode: 0644]
TLDI/Normals.agda [new file with mode: 0644]
TLDI/Terms.agda [new file with mode: 0644]
TLDI/TypeTheory/Bool.agda [new file with mode: 0644]
TLDI/TypeTheory/Empty.agda [new file with mode: 0644]
TLDI/TypeTheory/Function.agda [new file with mode: 0644]
TLDI/TypeTheory/List.agda [new file with mode: 0644]
TLDI/TypeTheory/Nat.agda [new file with mode: 0644]
TLDI/TypeTheory/Product.agda [new file with mode: 0644]
TLDI/TypeTheory/PropEq.agda [new file with mode: 0644]
TLDI/TypeTheory/StateMonad.agda [new file with mode: 0644]
TLDI/TypeTheory/Unit.agda [new file with mode: 0644]
TLDI/Types.agda [new file with mode: 0644]
TLDI/Values.agda [new file with mode: 0644]
TLDI/Weakening.agda [new file with mode: 0644]