Típuselmélet Kutatócsoport

2025.03.31.

Bemutatkozás

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

➥ Csoportvezető bemutatása (videó)

Kutatási területek

▶ Martin-Löf típuselméletének metaelmélete

alternatív szöveg — ➥ *Programs in a functional programming language at different levels of abstraction.* At each of the six levels of abstraction, a bubble represents a program. At level (1) a program is a string, this is the most concrete level, at level (6) a program is a well-typed syntax tree quotiented by conversion, this is the most abstract level.

Kapcsolódó publikációk:
https://doi.org/10.4230/LIPIcs.FSCD.2023.18
https://doi.org/10.1145/3290315
https://doi.org/10.4230/LIPIcs.FSCD.2024.10
https://doi.org/10.1145/3373718.3394770

▶ A típuselmélet bővítései: extenzionalitás, univalencia, parametricitás, új definicionális egyenlőségek

➥ *Illustration of representing an infinite-dimensional structure (above) by a finite diagram (left, below), and a syntax of a language coming directly from the finite diagram (right, below).*

Kapcsolódó publikációk:
https://doi.org/10.1145/3632920
https://doi.org/10.23638/LMCS-16(1:10)2020
https://doi.org/10.1007/978-3-030-71995-1_1

▶ A matematika számítógépes formalizálása

Kapcsolódó publikációk:
https://doi.org/10.4230/LIPIcs.FSCD.2023.24
https://doi.org/10.4230/LIPIcs.TYPES.2022.10

▶ Függő típusozású programozási nyelvek implementációja

Kapcsolódó publikációk:
https://doi.org/10.1145/3547641
https://doi.org/10.1145/3408983

Módszertan

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.

Kutatócsoport tagjai

(Kaposi Ambrus docens, 3 PhD hallgató, számos MSc és BSc hallgató.)

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

Nyertes pályázatok

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

Öt fontos publikáció

Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman: Internal Parametricity, without an Interval. Proc. ACM Program. Lang. 8(POPL): 2340-2369 (2024) https://doi.org/10.1145/3632920
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler: For the Metatheory of Type Theory, Internal Sconing Is Enough. FSCD 2023: 18:1-18:23 https://doi.or/10.4230/LIPIcs.FSCD.2023.18
András Kovács: Staged compilation with two-level type theory. Proc. ACM Program. Lang. 6(ICFP): 540-569 (2022) https://doi.org/10.1145/3547641
Ambrus Kaposi, András Kovács: Signatures and Induction Principles for Higher Inductive-Inductive Types. Log. Methods Comput. Sci. 16(1) (2020) https://doi.org/10.23638/LMCS-16(1:10)2020
Ambrus Kaposi, András Kovács, Thorsten Altenkirch: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL): 2:1-2:24 (2019) https://doi.org/10.1145/3290315

Elérhetőség

Kaposi Ambrus docens: akaposi@inf.elte.hu