Native Type Theory

Christian Williams
(University of California, Riverside)
Michael Stay
(Pyrofex Corporation, Utah)

Native type systems are those in which type constructors are derived from term constructors, as well as the constructors of predicate logic and intuitionistic type theory. We present a method to construct native type systems for a broad class of languages, lambda-theories with equality, by embedding such a theory into the internal language of its topos of presheaves. Native types provide total specification of the structure of terms; and by internalizing transition systems, native type systems serve to reason about structure and behavior simultaneously. The construction is functorial, thereby providing a shared framework of higher-order reasoning for many languages, including programming languages.

In Kohei Kishida: Proceedings of the Fourth International Conference on Applied Category Theory (ACT 2021), Cambridge, United Kingdom, 12-16th July 2021, Electronic Proceedings in Theoretical Computer Science 372, pp. 116–132.
Published: 3rd November 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: