Lambda-calculus with shift/reset. Isabelle/HOL mechanization.
Kenichi Asai, Ochanomizu University, 2005.

Calculus:
  - Call-by-value lambda-calculus with shift/reset, integers, fix-point

  - Type-and-effect typing, per Danvy/Filinski's 1989 technical report

  - No let-polymorphism

  - Small-step semantics with explicit contexts as a datatype

  - Semantics of shift is based on capturing of explicit context


Formalization:
  - Concrete syntax for variables; variables named by integers 

  - Explicit operations for context filling, explicit congruences

  - Cannot evaluate sample terms or infer their types, can check
    the types of the results of the evaluation

  - Proved subject reduction (type preservation in one-step evaluation)

  - Not proved progress

  - Not using the nominal package, but assuming that the substituted
    values are closed, to avoid alpha-renaming

  - Runs on the standard Isabelle/HOL


Files:

Syntax.thy	Syntax of the calculus
Env.thy		Environments: associating variables with values or types
Typing.thy	The well-typed relation and (long) proofs of substitution
		and context filling lemmas
Eval.thy	One-step evaluation relation and the proof of subject reduction