ipl

Agda formalization of Intuitionistic Propositional Logic (IPL)

Agda HTML listing.

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:

• PDF Handout
• Agda HTML listing

Soundness

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.

• Agda HTML listing.