Index-Stratified Types (Extended Version)
Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau

TL;DR
The paper introduces Tores, a core language with novel index-stratified types and well-founded recursion, enabling encoding of complex metatheoretic proofs like normalization, with proven soundness and termination.
Contribution
It presents Tores, a new core language featuring index-stratified types and Mendler-style recursion, advancing the encoding of metatheoretic proofs.
Findings
Proves soundness of Tores as a programming and proof language.
Demonstrates encoding of normalization proofs for lambda calculus.
Establishes termination and subject reduction theorems.
Abstract
We present Tores, a core language for encoding metatheoretic proofs. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types and a form of recursion over objects in the index language to build new types. The latter, which we call index-stratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies
