Type Theory

(Up) | See also: Type Systems

Works regarding the formal study of types, primarily in its original meaning as a means to avoid paradoxes in logic, and secondarily as it is studied in the modern world to provide a theoretical basis for type systems in programming languages.

Web resources

Type Theory (Stanford Encyclopedia of Philosophy) ★★ 💭

Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy) ★★ 💭

Does there exist a Turing complete typed lambda calculus? ★

Characterization of lambda-terms that have union types ★

Type Theory and Mathematical Logic | artagnon.com ★

Typed Combinators ★

Recursive Types for Free! (Philip Wadler) ★

Computational type theory - Scholarpedia

(in Type Systems) The algebra (and calculus!) of algebraic data types ★★★

Papers

Recursive Types (online @ www.ps.uni-saarland.de) ★ 💭

On Universes in Type Theory (online @ www2.math.uu.se, media.githubusercontent.com) ★ 💭

The Gentle Art of Levitation (online @ personal.cis.strath.ac.uk) ★ 💭

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega (online @ web.cs.ucla.edu)

A lean specification for GADTs: system F with first-class equality proofs (online @ link.springer.com) ★ 💭

Observational Equality, Now! (online @ strictlypositive.org) 💭

(in Calculus of Constructions) The Calculus of Inductive Constructions ★ 💭

(in Computational Complexity) The Typed Lambda Calculus is not Elementary Recursive (online @ www.cs.cornell.edu) ★

(in Name Binding) A Type and Scope Safe Universe of Syntaxes with Binding

(in Type Systems) Abstract Types have Existential Type (online @ homepages.inf.ed.ac.uk) 🏛️

Books

Basic Simple Type Theory (borrow with print disabilities @ archive.org) ★ 💭

Type Theory and Functional Programming (online @ www.cs.kent.ac.uk)

Programming in Martin-Löf’s Type Theory (online @ www.cse.chalmers.se)