Programming with Proofs: A Second Order Type Theory
Abstract elided by the publisher.
Related papers
- Large model constructions for second-order ZF in dependent type theory CPP 2018
- Hardware Verification using Monadic Second-Order Logic CAV 1995
- How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation ICFP 2017
- How to prove decidability of equational theories with second-order computation analyser SOL JFP 2019
- Empty Types in Polymorphic Lambda Calculus POPL 1987
- Canonicity for Indexed Inductive-Recursive Types POPL 2026
- Second-Order Unification and Type Inference for Church-Style Polymorphism POPL 1998
- A Theory of Second-Order Trees ESOP 2002