Agda formalization of Intuitionistic Propositional Logic (IPL)
Normalization by Evaluation for IPL, Call-By-Push-Value, and Polarized Lambda Calculus (without soundness)
The simple Normalization by Evaluation (NbE) algorithm that produces from every IPL (CBPV, resp.) derivation a normal derivation.
Version published 2019-02-16 on arXiv:
- Article Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
- Formalization of Section 2, NbE of IPL using a Cover Monad
- Formalization of (a variant of) Section 3, NbE for Call-by-Push-Value
- Partial formalization of Section 4, Syntax and Semantics of Polarized Lambda-Calculus
Version presented 2018-07-19 at the Initial Types Club:
Soundness of NbE means that the computational behavior (functional interpretation) of IPL proofs is preserved by normalization.
We implement sound-by-construction NbE using Kripke predicates.