Native Type Theory

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.