Type theory · foundations, languages, proof assistants and program logics

A connected history of type theory, programming languages, proof assistants and program logics, from Frege, Russell and Church to dependent types, homotopy type theory, cubical computation and recent higher-dimensional research. Gregorian calendar, UTC. Sources checked 3 November 2026.

Explore the families

Use Separate by tags to compare overlapping strands. Events are tagged for their theories, systems and application areas: foundations, polymorphism, dependent types, logical frameworks, proof assistants, program refinement, refinement types, separation logic, linear types, homotopy type theory, cubical type theory, programming languages and verified applications. Individual tags identify Coq/Rocq, Lean, Agda, Nuprl, HOL, Isabelle, F*, Idris, and other projects. The tracks share a calendar; they are not alternative histories or a single project ancestry tree.

Follow the theory into tools. Simple types and classical higher-order logic lead to the HOL family; LCF supplies a trusted-inference architecture. Constructive dependent foundations support Nuprl, constructions-based Coq/Rocq and other dependent programming systems. LF, Twelf, Beluga and Dedukti illustrate logical frameworks. Polymorphism, System F, ML inference, existential abstraction, System FC, gradual typing and DOT connect foundational research to programming-language implementation. Mizar, ACL2 and TLA are neighboring formal-methods traditions, included for comparison rather than incorrectly classed as HoTT descendants.

Program verification has several meanings of refinement. The timeline separates value-refinement types from specification-to-implementation refinement calculus and from interactive proof-goal refinement. Hoare logic, weakest preconditions, B, separation logic and Iris describe different correctness methods. Boogie, Z3, Dafny, Why3, Viper, F*, LiquidHaskell, Prusti, Creusot and Verus show different automation and language integrations. SMT solving, interactive proof checking and verified compilation have distinct trust boundaries.

HoTT, Coq and computational equality

The groupoid and homotopy interpretations of identity lead into univalent foundations and the HoTT Book. The HoTT Library in Coq and UniMath are separate libraries with related goals. Axiomatizing univalence in a configured Coq development does not make its kernel computationally cubical. Cubical models, CCHM, Cartesian computational higher type theory, RedPRL, cubical Agda, Arend and cooltt appear as distinct research or implementation milestones. Two-level, directed, modal, displayed and higher observational work extend the map further.

The lambda-cube cover compares typed calculi; it is not a diagram of cubical identity cells. Attached concept cards explain dependent Pi/Sigma types, judgmental equality versus identity proofs, universes, univalence, higher inductive types, canonicity versus normalization, usage quantities and verification boundaries. These notes explain concepts without adding fictitious dated events.

Dates, status and evidence

Each event states whether it is a manuscript, circulated note, publication, presentation, project milestone, compiler release or status snapshot. Publication dates do not automatically date invention. Howard’s 1969 circulation and 1980 publication, the 1973 colloquium and 1975 predicative paper, and the CCHM preprint and later TYPES 2015 proceedings publication are deliberately separated. The 2010 Voevodsky talk is not dated by its later arXiv deposit. Recent arXiv events are explicitly preprints, not claims of peer-reviewed acceptance. The cooltt marker records the repository as observed on 3 November 2026, not an inferred first-release year.

Year-only and month-only evidence uses January 1 or the first day solely as a plotting anchor. Midnight UTC does not assert a historical time of day. Coarse dates have presumptive outlines. Editorial coverage bands organize selected entries; they do not measure project lifetimes or claim that a line of research ended. The selection is extensive but cannot enumerate every calculus, language, proof library or implementation release.

Sources prioritize original papers, authors’ manuscripts, official histories, project repositories, release announcements and institutional records. Later author/project retrospectives are identified where needed. Each event has its own source list. Relationships carry explanations and supporting references in historyLinks metadata: arrows indicate specified theoretical or implementation relationships; comparison arcs distinguish related ideas without asserting descent. A relationship never implies that every feature of the target is derived from the source, or that the implementations are compatible.

Projects as evidence of use

Formalized mathematics includes the four-colour theorem, odd-order theorem, Flyspeck and mathlib. CompCert, seL4, CakeML, HACL*, EverCrypt and RustBelt demonstrate different verified-system or semantic-correctness achievements. MetaCoq/MetaRocq and Coq Coq Correct examine the checking and erasure machinery itself. Read the stated specification and assumptions: a theorem about one modeled component is not a blanket theorem about an entire deployed system.

Media credits

Individually checked Wikimedia Commons files use public-domain or Creative Commons attribution/share-alike licenses. Later portraits illustrate people rather than the historical date of the event. The modern HoTT Book cover illustrates the book. The lambda cube is an explanatory diagram, not a historical photograph or a cubical-theory logo.

• Tellofou · Lambda Cube img.svg · CC BY-SA 4.0; rights.
• Unknown author Unknown author · Bertrand Russell (c. April 1940).jpg.jpg) · Public domain; rights.
• Andrej Bauer · Per Martin-Lof May 2007.jpg · CC BY-SA 2.5 si; rights.
• Andrej Bauer · Thierry Coquand.jpg · CC BY-SA 2.5 si; rights.
• Schmid, Renate · VladimirVoevodsky.jpg · CC BY-SA 2.0 de; rights.
• The Univalent Foundations Program Institute for Advanced Study · Hott-a4.pdf · CC BY-SA 3.0; rights.