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)