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 19d ago