Type theory is a formal language which can be used as a programming
language [1] and also as a foundation for mathematics [2] replacing
first order logic and set theory. Its current form was described by
Per Martin-Löf in the 1970s [1]. There are several computer
implementations of type theory (also called proof assistants), the
most popular ones are Agda, Coq, Idris, Lean. These are functional
programming languages close in spirit to Haskell, ML, F#. Type theory
can be seen as an algebraic theory [3] (such as rings or vector
spaces), its important properties such as parametricity and canonicity
[4] can be proved algebraically. Interesting research areas include
the following.
- Efficient computer implementation of type theory. Lambda calculus,
type checking, elaboration, normalisation. See [5]
- Inductive and coinductive types in type theory. How to specify and
implement them? The syntax of type theory itself is an inductive
type. Turing machinges are coinductive. See [6,7]
- A type theory with function extensionality. How to prove its
metatheoretic properties? See [8] for a start.
The topic is very technical, it involves lots of syntactic
manipulation. Some people like to overcome this by computer-checking
every argument using proof assistants. Other people like to make it
very abstract using category theory [9].
Hivatkozások
- Per Martin-Löf, Constructive Mathematics and Computer Programming, Editor(s): L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, Klaus-Peter Podewski, Studies in Logic and the Foundations of Mathematics, Elsevier, Volume 104, 1982, Pages 153-175. https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf
- Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book
- Thorsten Altenkirch and Ambrus Kaposi. 2016. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16). Association for Computing Machinery, New York, NY, USA, 18–29. https://akaposi.github.io/tt-in-tt.pdf
- Ambrus Kaposi, Simon Huber, Christian Sattler: Gluing for Type Theory. FSCD 2019: 25:1-25:19. https://drops.dagstuhl.de/opus/volltexte/2019/10532/pdf/LIPIcs-FSCD-2019-25.pdf
- https://github.com/AndrasKovacs/elaboration-zoo
- ALTENKIRCH, T., GHANI, N., HANCOCK, P., MCBRIDE, C., & MORRIS, P. (2015). Indexed containers. Journal of Functional Programming, 25, E5. doi:10.1017/6S095679681500009X
- Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. 2019. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3, POPL, Article 2 (January 2019), 24 pages. DOI:https://doi.org/10.1145/3290315
- Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau: Setoid Type Theory - A Syntactic Translation. MPC 2019: 155-196. https://doi.org/10.1007/978-3-030-33636-3_12
- Steve Awodey. Category Theory, Oxford Logic Guides, Oxford University Press, 2006.