Type Theory

(Up) | See also: Type Systems

Web resources

Type Theory (Stanford Encyclopedia of Philosophy)

Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy)

computability - Does there exist a Turing complete typed lambda calculus? - Computer Science Stack Exchange

Characterization of lambda-terms that have union types - Computer Science Stack Exchange

Type Theory and Mathematical Logic | artagnon.com

Typed Combinators

Recursive Types for Free! (Philip Wadler)

Computational type theory - Scholarpedia

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)

Books

Basic Simple Type Theory (borrow @ 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)