Type Theory Research Group
We are developing new programming languages with dependent types and study the metatheory of such languages. For example, we study the different classes of inductive types, high level descriptions of programming languages as initial models of algebraic theories, extensional principles in type theory, homotopy type theory, strictness in type theory, efficient implementations of type checkers.
Group's own website: external link
▶ Metatheory of Martin-Löf’s type theory
Related publications:
☞ For the metatheory of type theory, internal sconing is enough
☞ Constructing quotient inductive-inductive types
☞ Second-order generalised algebraic theories: signatures and first-order semantics
☞ Large and infinitary quotient inductive-inductive types
▶ Extensions of type theory with extensionality, univalence, parametricity, new definitional equalities
Related publications:
☞ Internal Parametricity, without an Interval
☞ Signatures and Induction Principles for Higher Inductive-Inductive Types
☞ Constructing a universe for the setoid model
▶ Formalisation of mathematics in proof assistants
Related publications:
☞ Combinatory logic and lambda calculus are equal, algebraically
☞ The Münchhausen method in type theory
▶ Implementation of dependently typed programming languages and proof assistants
Related publications:
☞ Staged compilation with two-level type theory
☞ Elaboration with first-class implicit function types
Research methodology
The theoretical methods from the theory of programming languages and category theory, the proof assistants Agda and Coq are used. New softwares in Haskell and OCaml are developed.
Research staff
- Ambrus Kaposi associate professor
- Rafaël Bocquet PhD student
- Viktor Bense PhD student
- Szumi Xie PhD student
- Viktor Csimma BSc student
- Péter Zsolt Korpa MSc student
- Márton Petes MSc student
- Bálint Bence Török BSc student
- Zhenyun Yin BSc student
- Higher Observational Type Theory (HOTT) ERC Consolidator Grant
- COST action EuroProofNet CA20111
- „Application Domain Specific Highly Reliable IT Solutions” project of the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme
- COST Action EUTypes CA15123
- EFOP-3.6.3-VEKOP-16-2017-00002
- Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman: Internal Parametricity, without an Interval. Proc. ACM Program. Lang. 8(POPL): 2340-2369 (2024) [DOI]
- Rafaël Bocquet, Ambrus Kaposi, Christian Sattler: For the Metatheory of Type Theory, Internal Sconing Is Enough. FSCD 2023: 18:1-18:23 [DOI]
- András Kovács: Staged compilation with two-level type theory. Proc. ACM Program. Lang. 6(ICFP): 540-569 (2022) [DOI]
- Ambrus Kaposi, András Kovács: Signatures and Induction Principles for Higher Inductive-Inductive Types. Log. Methods Comput. Sci. 16(1) (2020) [DOI]
- Ambrus Kaposi, András Kovács, Thorsten Altenkirch: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL): 2:1-2:24 (2019) [DOI]
Ambrus Kaposi associate professor: akaposi@inf.elte.hu