Típuselmélet kutatócsoport
Kutatócsoportunkban függő típusokkal rendelkező programozási nyelveket fejlesztünk és ezek metaelméletét tanulmányozzuk. Többek között foglalkozunk az induktív típusok különböző osztályaival; a formális nyelvek magas szintű, algebrai leírásával; homotópia-típuselmélettel; az egyenlőség extenzionalitási tulajdonságaival és szigorúságával; hatékony típusellenőrzők implementációjával.
Csoport saját honlapja: külső link
▶ Martin-Löf típuselméletének metaelmélete
Kapcsolódó publikációk:
☞ 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
▶ A típuselmélet bővítései: extenzionalitás, univalencia, parametricitás, új definicionális egyenlőségek
Kapcsolódó publikációk:
☞ Internal Parametricity, without an Interval
☞ Signatures and Induction Principles for Higher Inductive-Inductive Types
☞ Constructing a universe for the setoid model
▶ A matematika számítógépes formalizálása
Kapcsolódó publikációk:
☞ Combinatory logic and lambda calculus are equal, algebraically
☞ The Münchhausen method in type theory
▶ Függő típusozású programozási nyelvek implementációja
Kapcsolódó publikációk:
☞ Staged compilation with two-level type theory
☞ Elaboration with first-class implicit function types
A programozási nyelvek és a kategóriaelmélet elméleti eszköztárának, az Agda és Coq bizonyító-asszisztenseknek, továbbá a Haskell és OCaml programozási nyelveknek a használata.
- Kaposi Ambrus, docens
- Rafaël Bocquet PhD hallgató
- Bense Viktor PhD hallgató
- Csimma Viktor PhD hallgató
- Korpa Péter Zsolt MSc diák
- Petes Márton MSc diák
- Török Bálint Bence BSc diák
- Szumi Xie PhD diák
- Zhenyun Yin BSc diák
- 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]