Type Theory
(Up) | See also: Type Systems
Web resources
Type Theory (Stanford Encyclopedia of Philosophy) ★★ 💭
Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy) ★★ 💭
Characterization of lambda-terms that have union types - Computer Science Stack Exchange ★
Type Theory and Mathematical Logic \| artagnon.com ★
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 Term Rewriting) The Rho Cube
(in Type Systems) Abstract Types have Existential Type (online @ homepages.inf.ed.ac.uk) 🏛️
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)