18 citations · 18 across the 4 of their papers we have counts for
4 papers
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…
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…
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…
Impredicative Encodings of (Higher) Inductive Types
Steve Awodey, Jonas Frey, Sam Speight
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and…