Abstracts.2021.NbE.STLC

Normalization-by-Evaluation for the Simply-typed Lambda Calculus

by Andreas Abel

Abstract

TBD

Resources

Related reading:

• Andreas, Normalization by Evaluation for Intuitionistic Propositional Logic

Related ITC talks:

• Andreas, From Normalization by Evaluation to Call-By-Push-Value
• Nachi, Normalization for typed lambda calculus with co-products
• Frederik, Kripke-style semantics for simply typed lambda calculus

Related implementations:

• Andras Kovacs, A Machine-Checked Correctness Proof of Normalization by Evaluation for Simply Typed Lambda Calculus
• Andreas Abel, Normalization by Evaluation for IPL, Call-By-Push-Value, and Polarized Lambda Calculus (without soundness)

References

TBD

Bibliography

• Wim Veldman. An Intuitionistic Completeness Theorem for Intuitionistic Predicate Logic. J. Symb. Log. 41(1), pp. 159-166, 1976. Notes: Intuitionistic logic with positive formulas ⊥ and A ∨ B, Kripke models with "exploding nodes".

• Thorsten Altenkirch, Martin Hofmann, Thomas Streicher. Categorical Reconstruction of a Reduction Free Normalization Proof. Category Theory and Computer Science 1995, pp. 182-199, 1995.
• Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott. Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS 2001, pp. 303-310, 2001.