HackerPapers

arXiv:2102.04672cs.LO

Native Type Theory

Christian Williams, Michael Stay

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
In Proceedings ACT 2021, arXiv:2211.01102
Journal reference
EPTCS 372, 2022, pp. 116-132
DOI
doi:10.4204/EPTCS.372.9
Subjects
cs.LOLogic in Computer Science math.CTCategory Theory

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Feb 2021 to Feb 2021.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Native Type Theory 1 comment

    • > For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types are expressive and pervasive, yet…

      sirabenView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.