Ambrus Kaposi

Teaching   Advertisements   Drafts and publications   Talks

I am an assistant professor at the Department of Programming Languages and Compilers, Faculty of Informatics, Eötvös Loránd University, Budapest, Hungary. I have a bachelor's degree in computer science from the same university and a PhD in type theory from the University of Nottingham. Previously I did a PhD on medical statistics after becoming a medical doctor at Semmelweis University.

Email: akaposi@inf.elte.hu

Address: Kaposi Ambrus
ELTE-IK, Programozási Nyelvek és Fordítóprogramok Tanszék
Pázmány Péter sétány 1/C
1117 Budapest
Hungary

Room: 2-620 in the South Building (location of building, map of building). After 17.30 the door in the corridor is locked, you can use the interphone next to the door.

Office hours (fogadóóra): Monday 17.00-19.00

Teaching

Current teaching at Eötvös Loránd University:

Past teaching:

Advertisements

Budapest type theory seminar once a week, very informal, everyone is welcome to join.

If you are interested in functional programming or type theory, the best way to learn and get involved is to go to one of the following excellent (summer) schools. Usually they have scholarships for student attendees.

Student and research projects (TDK, szakdolgozat témák) include the following:

Drafts and publications

Any comments are very much welcome. List of all publications, some bibtex items.

Setoid type theory
Draft, 2018
Constructing Quotient Inductive-Inductive Types
with Thorsten Altenkirch and András Kovács
POPL 2019
formalisation
A syntax for higher inductive-inductive types
with András Kovács
FSCD 2018, received Best Paper Award for Junior Researcher
formalisation
Codes for quotient inductive-inductive types
with András Kovács
Draft, Oct 2017
A fröccs szintaxisa és operációs szemantikája
ELTE Fröccs Akadémia, 2017
formalisation
Normalisation by Evaluation for Type Theory, in Type Theory
with Thorsten Altenkirch
LMCS, 2017
formalisation
Type theory in a type theory with quotient inductive types
PhD thesis, date of defence: 24 Nov 2016
Advisor: Graham Hutton
formalisation
Normalisation by Evaluation for Dependent Types
with Thorsten Altenkirch
FSCD 2016
formalisation
Type Theory in Type Theory using Quotient Inductive Types
with Thorsten Altenkirch
POPL 2016
formalisation
Towards a cubical type theory without an interval
with Thorsten Altenkirch
TYPES 2015 post-proceedings
Formalising the completeness theorem of classical propositional logic in Agda
with Leran Cai and Thorsten Altenkirch
Draft, Mar 2015
Free Applicative Functors
with Paolo Capriotti
MSFP 2014
comments
Bevezetés a homotópia-típuselméletbe
Tízéves az ELTE Eötvös József Collegium Informatikai Műhelye, 2014
First year report
An introduction to type theory with a notation using De Bruijn indices and explicit substitutions. Nov 2013.

Talks

Induction-induction Part 3
TYPES, Braga, 21 June 2018
abstract
Specifying higher inductive-inductive types
Université de Nantes, 25 April 2018
A syntax for higher inductive-inductive types
Agda Implementors' Meeting, Budapest, 31 January 2018
A syntax for higher inductive-inductive types
EUTypes Working Meeting, Nijmegen, 23 January 2018
Bizonyítás és programozás
Pannonhalmi Bencés Gimnázium, 24 November 2017
Normalisation by Evaluation for a Type Theory with Large Elimination
TYPES, Budapest, 30 May 2017
abstract
Formalising the metatheory of type theory using quotient inductive types
FPFM, Nantes, 27 April 2017
Normalisation by evaluation for an intrinsic syntax of type theory
EUTypes Meeting, Ljubljana, 31 Jan 2017
Normalisation by Evaluation for Dependent Types
FSCD, Porto, 24 June 2016
Normalisation by Evaluation for Dependent Types
TYPES, Novi Sad, 25 May 2016
abstract
Type theory in type theory using quotient inductive types
Theoretical computer science seminar, University of Birmingham, 26 Feb 2016
Type Theory in Type Theory using Quotient Inductive Types
POPL, St Petersburg, Florida, 20 Jan 2016
poster
video
A nominal syntax for internal parametricity
TYPES, Tallinn, 21 May 2015
abstract
Bevezetés a homotópia-típuselméletbe
Eötvös Kollégium, Budapest, 7 Jan 2015
Bizonyítás és programozás
Hackerspace, Budapest, 6 Jan 2015
A syntax for cubical type theory
with Thorsten Altenkirch
HoTT Workshop, Oxford, 8 Nov 2014
video
A syntax for cubical type theory
University of Bath, 4 Nov 2014
A syntax for cubical type theory
AIM XIX, Paris, 23 May 2014
Bevezetés a homotópia-típuselméletbe
Tízéves az ELTE Eötvös József Collegium Informatikai Műhelye Konferencia, Budapest, 21 Feb 2014

Last modified: 8 Oct 2018