Ambrus Kaposi

Advertisements   Drafts and publications   Talks   Teaching   Activities

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

Room: 2-705 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): Tuesday 10-12.

Advertisements

Budapest type theory seminar: every Tuesday evening 19:00 at ELTE Lágymányos Déli épület 4-429, contact me if you want to come, and I'll add you to the mailing list. Greenboard photos.

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):

Drafts and publications

Any comments are very much welcome.

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 postproceedings
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.

List of all publications

Talks

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
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

Teaching

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

Past teaching:

Activities


Last modified: 9 June 2017