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