Added work on "shapes" semantics for dynamism. master
authorJoey Capper <jjc@cs.nott.ac.uk>
Fri, 26 Jul 2013 02:37:36 +0000 (03:37 +0100)
committerJoey Capper <jjc@cs.nott.ac.uk>
Fri, 26 Jul 2013 02:37:36 +0000 (03:37 +0100)
commit221e0f2875f1a732b6ff20a86a5847981fe98c95
treec824d6c9d20445a7d9cc4dc2ffac786d42411135
parentae57df3e02567ed3cf2be3e42f2fb28c41ecc1a5
Added work on "shapes" semantics for dynamism.
29 files changed:
TLDI Dynamism/Contexts.agda [new file with mode: 0644]
TLDI Dynamism/Convertibility.agda [new file with mode: 0644]
TLDI Dynamism/Examples/BreakingPendulum.agda [new file with mode: 0644]
TLDI Dynamism/Examples/Core.agda [new file with mode: 0644]
TLDI Dynamism/Examples/Electrical.agda [new file with mode: 0644]
TLDI Dynamism/Examples/Mechanics.agda [new file with mode: 0644]
TLDI Dynamism/FHM.agda [new file with mode: 0644]
TLDI Dynamism/FlatEquations.agda [new file with mode: 0644]
TLDI Dynamism/Infer.agda [new file with mode: 0644]
TLDI Dynamism/Iteration.agda [new file with mode: 0644]
TLDI Dynamism/Labeling.agda [new file with mode: 0644]
TLDI Dynamism/Normalisation.agda [new file with mode: 0644]
TLDI Dynamism/Normals.agda [new file with mode: 0644]
TLDI Dynamism/TermShape.agda [new file with mode: 0644]
TLDI Dynamism/Terms.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Bool.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Empty.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Fin.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Function.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/List.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Nat.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Product.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/PropEq.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/StateMonad.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Unit.agda [new file with mode: 0644]
TLDI Dynamism/TypeTheory/Vector.agda [new file with mode: 0644]
TLDI Dynamism/Types.agda [new file with mode: 0644]
TLDI Dynamism/Values.agda [new file with mode: 0644]
TLDI Dynamism/Weakening.agda [new file with mode: 0644]