CIS 6700: Type Systems - Spring 2025

Project proposal

For my semester project, I am mechanizing strong normalization of simply-typed CPBV lambda calculus, following this paper¹, but with the following differences:

• The mechanization will be in Lean instead of Rocq. This is mostly because I recently implemented a mutual induction tactic for Lean, and CPBV involves a lot of mutually defined inductives, so it would be a good test case.
• The proof technique will follow what I did in Homework #6, using the definition of strong normalization from POPLMark reloaded². The idea of saturation in terms of neutral and normal forms was clearer to me, and it would be interesting to see how it extends to CBPV with values and computations being explicitly separate.

As a further extension, I have an additional idea:

• The let expressions in CBPV apparently subsume monadic normal form (MNF)³. In terms of compiler passes, usually the next step is linearizing the computations to some ANF, but this paper⁴ shows how to do a imperativization pass first (i.e. turning lets into set!s), followed by an "AB-normalization" pass, which easily linearizes the set!s. It would be interesting to see how this applies to CBPV, and what the type system for an "imperative CBPV" language might look like after the first pass. (The AB-normal form is subsumed by it, so its type system after the second pass should be the same.)

---

1. Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark. Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory. https://www.ps.uni-saarland.de/Publications/documents/ForsterEtAl_2018_Call-By-Push-Value.pdf. ↩︎

2. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. POPLMark reloaded: Mechanizing proofs by logical relations. https://poplmark-reloaded.github.io/pdf/main.pdf. ↩︎

3. Max S. New. Compiling with Call-by-push-value. https://coalg.org/calco-mfps-2023/slides/compiling-with-cbpv-1.pdf. ↩︎

4. William J. Bowman. A Low-Level Look at A-Normal Form. https://www.williamjbowman.com/resources/wjb2024-anf-is-dead.pdf. ↩︎