2025.09.17.
Típuselmélet kutatócsoport
type-theory-thumb-702x456-.png

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őt és a kutatási témát bemutató kisfilm

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:
 ☞ 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
➥ 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:
 ☞ 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

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 (kutatócsoport-vezető) [MTMT, Tud-O-Méter]
  • Rafaël Bocquet PhD hallgató
  • Bense Viktor PhD hallgató [MTMT]
  • 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 [MTMT]
  • Zhenyun Yin BSc diák

Nyertes pályázatok

Kiemelt publikációk

  • Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman (2024): Internal Parametricity, without an Interval, Proc. ACM Program. Lang. [DOI]
  • Rafaël Bocquet, Ambrus Kaposi, Christian Sattler (2023): For the metatheory of type theory, Internal Sconing Is Enough. FSCD [DOI]
  • András Kovács (2022): Staged compilation with two-level type theory. Proc. ACM Program. Lang. [DOI]
  • Ambrus Kaposi, András Kovács (2020): Signatures and induction principles for higher inductive-inductive types. Log. Methods Comput. Sci. [DOI]
  • Ambrus Kaposi, András Kovács, Thorsten Altenkirch (2019): Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. [DOI]

Elérhetőség

Kaposi Ambrus – akaposi@inf.elte.hu

type-theory-thumb-702x456-.png