Lambda-calculus with shift/reset. Locally nameless Coq mechanization.
Noriko Hirota and Kenichi Asai, Ochanomizu University,
December 2007 - January 2008.
Calculus:
- Call-by-value lambda-calculus with shift/reset, no fix, no constants
- Type-and-effect typing, per Asai/Kameyama, APLAS 2007
- let-polymorphism
- Small-step semantics with NO explicit contexts
- Essentially bubbling-up semantics of shift
Formalization:
- Locally nameless syntax for variables
- Cannot evaluate sample terms or infer their types, can check
the types or the results of the evaluation
- Proved subject reduction (type preservation in one-step evaluation)
- Proved progress
Files:
nori_Definitions.v Definitions of terms, types, type schemas,
type judgments
Type checking and evaluation relations
Definitions of progress and preservation properties
nori_Infrastructure.v Lemmas and tactics, mostly about substitutions
nori_Soundness.v Lemmas about type substitutions, weakening
nori_preservation.v The proof of subject reduction
nori_progress.v The proof of progress
Makefile How to build it all
The following set of files by Brian Aydemir and Arthur Chargue'raud (2007)
are included for the sake of completeness.
They have been downloaded from the Mini-ML (core only) development
available at
http://www.chargueraud.org/arthur/research/2007/binders/
and are used in the shift/reset development unchanged.
Lib_FinSet.v
Lib_FinSetImpl.v
Lib_ListFacts.v
Lib_ListFactsMore.v
Lib_MyFSetInterface.v
Lib_Tactic.v
Metatheory.v
Metatheory_Env.v
Metatheory_Fresh.v
Metatheory_Var.v