Type theory

Témavezető:	Kaposi Ambrus
	Faculty of Informatics, ELTE
email:	akaposi@ik.elte.hu

Projekt leírás

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

1. 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
2. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book
3. 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
4. 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
5. https://github.com/AndrasKovacs/elaboration-zoo
6. ALTENKIRCH, T., GHANI, N., HANCOCK, P., MCBRIDE, C., & MORRIS, P. (2015). Indexed containers. Journal of Functional Programming, 25, E5. doi:10.1017/6S095679681500009X
7. 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
8. 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
9. Steve Awodey. Category Theory, Oxford Logic Guides, Oxford University Press, 2006.

Korábbi hallgatók

• Alexy Marcell: Type theory (2021/22 I. félév Egyéni Kutatómunka 1)
• Alexy Marcell: Type theory (2021/22 II. félév Egyéni Kutatómunka 2)