A Formalized Proof of Strong Normalization for Guarded Recursive Types
No abstract available.
DOI 10.1007/978-3-319-12736-1_8
Related papers
- Towards Strong Normalization for Dependent Object Types (DOT) ECOOP 2017
- Well-founded recursion with copatterns and sized types JFP 2016
- A compiled implementation of strong reduction ICFP 2002
- Wellfounded recursion with copatterns: a unified approach to termination and productivity ICFP 2013
- Bisimulation as path type for guarded recursive types POPL 2019
- Theoretical Pearls: A bargain for intersection types: a simple strong normalization proof JFP 2005
- Termination of rewriting in the Calculus of Constructions JFP 2003
- Modular Proof of Strong Normalization for the Calculus of Constructions JFP 1991