Kaposi Ambrus

A típuselmélet egy programozási nyelv olyan erős statikus típusrendszerrel, melyben tetszőleges matematikai állítás leírható típusként. Adott típusú program a típusnak megfelelő állítás bizonyításának tekinthető. A típuselmélet számítógépes implementációi így matematikai bizonyítások ellenőrzésére és bizonyítottan helyes programozásra is alkalmasak. Kutatásom fókuszában a típuselmélet alkalmazásai, metaelméleti tulajdonságai, implementációi és továbbfejlesztési lehetőségei állnak.

Kulcsszavak

típuselmélet, logika, számítástudomány, funkcionális programozás

Kiemelt publikációk

2019 – Kaposi, Ambrus; Kovács, András; Altenkirch, Thorsten – Constructing quotient inductive-inductive types – mtmt.hu
2016 – Altenkirch, Thorsten; Kaposi, Ambrus – Type theory in type theory using quotient inductive types – mtmt.hu
2020 – Kaposi, Ambrus; Kovács, András – Signatures and Induction Principles for Higher Inductive-Inductive Types – mtmt.hu
2017 – Altenkirch, Thorsten; Kaposi, Ambrus – Normalisation by Evaluation for Type Theory, in Type Theory – mtmt.hu
2024 – Altenkirch, Thorsten; Chamoun, Yorgo; Kaposi, Ambrus; Shulman, Michael – Internal Parametricity, without an Interval – mtmt.hu