3 citations · 4 across the 2 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2019★ 3 cited
Cocon: Computation in Contextual Type Theory
Brigitte Pientka, Andreas Abel, Francisco Ferreira +2
We describe a Martin-Löf style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOA…
cs.PL2018
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…