Ambrus Kaposi
Ambrus Kaposi
Habil. Associate Professor
Institute of Computer Science
lecturer
Department of Programming Languages and Compilers
lecturer
Contact details
Address
1117 Budapest, Pázmány Péter sétány 1/c.
Room
2-620
Phone/Extension
8497
Links
ORCID
0000-0001-9897-8936
WoS
H-5385-2017
Scopus
23485681600
Google Scholar
3FcTiVUAAAAJ
Publications
mtmt.hu
Szakmai honlap
http://akaposi.web.elte.hu
Doktori.hu
doktori.hu
  • 1. Natural sciences
    • 1.1 Mathematics
      • Pure mathematics
  • 1.2 Computer and information sciences
    • Computer sciences
Type theory

Type theory is a programming language featuring a strong static type system capable of encoding arbitrary mathematical propositions as types. A program of a given type can be seen as a proof of the corresponding proposition. Thus, computer implementations of type theory an be used as proof checkers and as languages for provably correct programming. My research focuses on applications, metatheory, implementations and extensions of type theory.

Keywords
logic, type theory, theory of computation, functional programming
  • 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