Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Impredicativity in Linear Dependent Type Theory
Sam Speight, Niels van der Weide
We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, w…
cs.LO2024
Groupoidal Realizability for Intensional Type Theory
Sam Speight
We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry non-trivial (non-discrete) homotopical structure. In the spirit o…