2 papers
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…
math.CT2026
A Structural Account of Combinatory Completeness
Ivan Kuzmin, Chad Nester, Ãlo Reimaa +1
We give a general notion of combinatory completeness with respect to a faithful cartesian club and use it systematically to obtain characterisations of a number of different kinds…