Index-Stratified Types (Extended Version)

Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau

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…