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