Type Theory

Notes

A value is some concrete thing, and a type is a collection of concrete things (but is itself not a concrete thing. For example any individual integer is a value, but the collection of all integers is a type. Much like elements and sets in set theory.

A type is a collection of values which inhabit that type. A type is a value which is a member of the type of types.

Type theory goes much much further than just tagging data.

The type determines which data structure you use.

Dependent types is basically about being able to express arbitrary things in your type system, meaning that you can construct arbitrary proofs. That's how Coq, Agda and Idris work.

Types are types and propositions are propositions; types come from programming languages, and propositions from logic, and they seem to have no relation to each other.

Links

SymmetryBook - Undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

[Timeline for Logic, λ-Calculus, and Programming Language Theory (2012)(http://fm.csl.sri.com/SSFT15/Timeline.pages.pdf) (HN)

PRL Project - Implementing computational mathematics and providing logic-based tools that help automate programming.

Hoare Type Theory - Contains the main libraries of Hoare Type Theory (HTT) for reasoning about sequential heap-manipulating programs.

Algorithm W Step by Step (2006) - Implementation of the classic algorithm W for Hindley- Milner polymorphic type inference in Haskell.

Alg - Program that generates all finite models of a first-order theory. It is optimized for equational theories.

Linear ML - Small implementation of a linear type theory in the style of the Benton-Wadler adjoint calculus.

Higher-Dimensional Type Theory Course (2020) - Graduate seminar course on the recent development of higher-dimensional type theory. (Code)

Last modified 14d ago