4 papers
Substructural Parametricity
C. B. Aberlé, Chris Martens, Frank Pfenning
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary lo…
Polynomial Universes in Homotopy Type Theory
C. B. Aberlé, David I. Spivak
Awodey, later with Newstead, showed how polynomial functors with extra structure (termed ``natural models'') hold within them the categorical semantics for dependent type theory. T…
Parametricity via Cohesion
C. B. Aberlé
Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In re…
Foundations of Substructural Dependent Type Theory
C. B. Aberlé
This paper presents preliminary work on a general system for integrating dependent types into substructural type systems such as linear logic and linear type theory. Prior work on…