POPLMark reloaded: Mechanizing proofs by logical relations
summary
Proposes a benchmark that mechanizes logical-relation proofs by proving strong normalization via Kripke-style logical relations for simply-typed lambda calculus formulated on well-typed terms; implements and compares the development in Beluga, Coq, Agda (three systems), reuses Autosubst 2 and generic-syntax libraries, builds a Beluga Harpoon development, and surfaces concrete outcomes: successful mechanizations, exposed coverage/termination bugs, missing library lemmas, and a corroborating F* solution.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:56The problem: Proofs are tricky to write
- 1:50Goal: Using a benchmark problem...
- 2:23POPL Mark Challenge: Mechanize System F
- 3:00POPL Mark Challenge: The Flip Side
- 3:30Contributions
- 4:58Considerations and Target Audience
- 6:10How to Define Strong Normalization?
- 7:31Beluga: Proof and Programming Environment based on contextual HOAS
- 8:11Coq Using de Bruijn with and without Autosubst 2
- 9:11Agda Using Well-typed de Bruijn with Generic-Syntax Library
related talks
45mLogic Meta Programming for Functional Languages
01h 34mFormal Logic Undressed
19mAutomated Verification of Fundamental Algebraic Laws
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
01h 03mVerifying Dependent Type-checkers
29mMechanized monadic equational reasoning for ML references
24mCode Extraction from Coq to ML-like languages
19mExtensible Metatheory Mechanization via Family Polymorphism