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

TL;DR
This paper introduces a method to construct native type systems for lambda-theories with equality by embedding them into their topos of presheaves, enabling unified reasoning about structure and behavior.
Contribution
It presents a functorial construction of native type systems that unify structural and behavioral reasoning across various languages, including programming languages.
Findings
Provides a systematic way to embed lambda-theories into presheaf topoi
Enables reasoning about term structure and behavior simultaneously
Offers a shared higher-order reasoning framework for multiple languages
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
