28 citations · 116 across the 28 of their papers we have counts for
Showing 2020Show all
3 papers · 1 filter
cs.LO2020★ 5 cited
Syntactic categories for dependent type theory: sketching and adequacy
Daniel Gratzer, Jonathan Sterling
We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one m…
cs.PL2020
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Jonathan Sterling, Robert Harper
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental…
cs.LO2020★ 10 cited
A Cubical Language for Bishop Sets
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity…