18 citations · 18 across the 4 of their papers we have counts for
Showing cs.LOShow all
3 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…
cs.LO2018★ 18 cited
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…