Triangulating Context Lemmas

Agda formalisation to accompany the paper ``Triangulating Context Lemmas" by Craig McLaughlin, James McKinna and Ian Stark.

Dependencies:

Agda version 2.5.1, 2.5.2 or 2.5.3
Agda standard library v0.12, v0.13 or v0.14

Example Installation Procedure

Agda 2.5.2 is compatible with GHC 8.0.2 and is available through the latest Long-Term Support release of the Haskell Tool Stack, with the following command line.

stack --resolver=lts-9.10 install Agda-2.5.2

The main results are summarised in triangulating-context-lemmas.agda.

Name		Name	Last commit message	Last commit date
Latest commit History 89 Commits
README.md		README.md
acmm.agda		acmm.agda
asc-apx.agda		asc-apx.agda
big-step-prop.agda		big-step-prop.agda
ciu-apx.agda		ciu-apx.agda
frm-stk-prop.agda		frm-stk-prop.agda
lambda-fg.agda		lambda-fg.agda
obs-apx.agda		obs-apx.agda
relations.agda		relations.agda
renaming-acmm.agda		renaming-acmm.agda
semantics-acmm.agda		semantics-acmm.agda
sim-fusion-lemmas.agda		sim-fusion-lemmas.agda
sim-fusion.agda		sim-fusion.agda
substitution-acmm.agda		substitution-acmm.agda
tri-big-step.agda		tri-big-step.agda
tri-frm-stk.agda		tri-frm-stk.agda
tri-prelude.agda		tri-prelude.agda
triangulating-cxt-lemmas.agda		triangulating-cxt-lemmas.agda
vcc-apx.agda		vcc-apx.agda

cmcl/triangulating-context-lemmas

Folders and files

Latest commit

History

Repository files navigation

Triangulating Context Lemmas

Example Installation Procedure

About

Resources

Stars

Watchers

Forks

Languages