Type Theory Group

Eötvös Loránd University, Budapest

Members Seminar Teaching Theses and publications HOTT ERC project

We are part of the Department of Programming Languages and Compilers at the Faculty of Informatics. We are developing new programming languages with dependent types and study the metatheory of such languages. For example, we study the different classes of inductive types, high level descriptions of programming languages as initial models of algebraic theories, extensional principles in type theory, homotopy type theory, strictness in type theory, efficient implementations of type checkers.

Members

Current members:

Budapest type theory seminar

General information:: Everyone is welcome!

Schedule

2026-??-?? Johann: 2-sortification (?)
2026-07-01 Boti: Axiomatic quantum field theories
2026-06-25 Daniël Otten: ???
2026-06-17 Geri: A coherent definition of simply-typed lambda calculus
2026-06-10 Janet: Normalisation of simply-typed lambda calculus with semi-weak sums
2026-06-03 (no seminar, HoTT/UF & MFPS & SSTT)
2026-05-27 Judit Madarász: A Proof of Andréka-Németi's Conjecture That Special Relativity Is the Only Possible Conceptual Reduct of Classical Kinematics
2026-05-26 Thorsten Altenkirch: A definition of the real interval using a higher coinductive type
2026-05-20 François-René ÐVB Rideau (Faré): Lambda, the Ultimate Paradigm. Slides. First-class implementations. Slides
2026-05-13 Peti: Sheaf model of first-order logic. Photos
2026-05-06 (no seminar, TYPES)
2026-04-29 Gergely: Towards a dependently-typed imperative language
2026-04-22 Kristof: Quillen model structures
2026-04-15 Niels van der Weide: The internal languages of univalent categories. Photos
2026-04-08 András Kovács: Simplest countermodel of funext. GitHub repo | Photos
2026-04-02 (Thursday!) Watching Szumi's HoTTEST
2026-03-25 Szumi: Introduction to observational type theory. Original OTT paper | Pujet's thesis | Photos
2026-03-18 Ambrus: A Modal Deconstruction of Löb Induction (Daniel Gratzer). Paper | Daniel's slides | Photos
2026-03-11 Ambrus: SOGATs by example. Photos
2026-03-04 Kristof: (Andréka, Madarász, Németi. Mutual deﬁnability does not imply deﬁnitional equivalence, a simple example). Photos
2026-02-25 Szumi: Category CwFs. Photos
2026-02-18 (Wednesday!) Jean. An order-reversing embedding of Turing degrees into effective modalities. Slides
2026-02-09 Ján Perháč. Proof Assistants for Education. Slides
2026-02-02 Samuel Novotny. An Introduction to Transparent Intensional Logic. Slides
2026-01-27 (Tuesday!) Szumi Xie. Introduction to cubical type theory. Photos
2026-01-19 Mabel Najdovski. Reconstructing the strict presheaf model of Pierre-Marie Pédrot (prefascist model) using abstract nonsense. Photos
2026-01-12 Gergely Buday. Tutorial of the Isar Structured Proof Language. Slides
2026-01-09 World Logic Day, Pécs, attendees from our group: Ambrus, András, Boti, David, Gergely, Janet, Jean, Kristóf, Peti, Roland, Stefania, Szumi, Viktor. Website
2026-01-06 (Tuesday!) Áron Szabó. Numerical instability or something more fundamental?
2025-12-08 Péter Korpa. Implementing datatypes via rewrite rules. Repository
2025-12-05 Rafaël Bocquet PhD defence and Saint Nicholas HOTT workshop
- 10:00 Rafaël Bocquet PhD defence
- around 12:30 lunch in Science Park Étterem, then coffee at TTK Étterem
- 14:00--15:00 Nicolai Kraus. Constructive ordinals and generalised decidability
- 15:00--16:00 Rafaël Bocquet. Normalization proofs in the presence of non-linear computation rules
- 16:00--16:30 (coffee break)
- 16:30--16:50 Ambrus Kaposi. Reedy fibrant presheaf model
- 16:50--17:10 Szumi Xie. Reduction of inductive-inductive types without UIP
- 17:10--17:30 David Berry. Category theory using QPERs
- 17:30--17:50 Botond Mészáros. Generalisations of gluing
- 17:50--18:10 Jean Abou-Samra. Deriving all QIITs from a single QIIT in an intensional setting
- 18:10-- pub time
2025-12-01 Kristóf Kanalas. Digital whiteboard.
2025-11-24 Viktor Bense. Second simplest countermodel of funext. GitHub repo
2025-11-17 Ambrus Kaposi. What is the difference between GATs and ATs?
2025-11-10 Jean Abou Samra: Model of countable reals. Slides
2025-11-03 Kálmán Kéri. Concatenative process calculus. Slides
2025-10-27 Patrik Jansson. Finite permutations in Agda. Slides. Agda-ventures with PolyP. Slides | More info
2025-10-20 Pierre-Marie Pédrot. A dependently-typed Dialectica translation. Slides
2025-10-13 Awodey book 8 Categories of Diagrams (Boti).
2025-10-06 Stefania Damato. Formalising inductive and coinductive containers. Slides
2025-09-29 Beth model club (Palmgren: Constructive sheaf semantics)
2025-09-22 Awodey book 7 Functors and naturality (Jean).
2025-09-17 Discussion of topics
2025-07-03 Awodey book 7b Functors and naturality (Janet).
2025-06-26 David Berry: (Q)PERs. Digital whiteboard.
2025-06-19 Awodey book 7a Functors and naturality (Janet).
2025-06-12 (TYPES in Glasgow)
2025-06-05 (Ambrus in Nottingham)
2025-05-26--2025-05-31 Agda Implementors' Meeting XL
2025-05-22 Thorsten Altenkirch. On category containers.
2025-05-15 Discussion about strict presheaves
2025-04-24 Awodey book 6b Exponentials (Gábor). Photos
2025-04-10 Awodey book 6a Exponentials (Gábor). Photos
2025-04-03 Awodey book 5c Limits and colimits (Szumi). Photos
2025-03-27 Awodey book 5b Limits and colimits (Szumi). Photos
2025-03-20 Péter Diviánszky. The Csip compiler.
2025-03-17 14.00-16.00 Room 0-817 (Dudich Endre). Sergei Soloviev. Asymmetry in Semantic Games. Abstract | Slides
2025-03-13 Awodey book 5a Limits and colimits (Szumi). Photos
2025-03-06 Ambrus Kaposi. Type theory vs. set theory. Article (Hungarian)
2025-02-27 Ambrus Kaposi. Prefascist strictification of CwFs. Draft paper
2025-02-20 Ambrus Kaposi. Call by value lambda calculus algebraically. Photos
2025-02-13 Awodey book 4c Groups and categories (Viktor). Photos Category without products with exponentials. Photo
2025-01-13 Szumi Xie. Second-order generalized algebraic theories. Abstract Ambrus Kaposi. Type theory as a SOGAT. Photo
2025-01-06 András Kovács. Runtime code generation with dependent types. Github repo
2024-12-20 Christmas type theory workshop. Location: D-1-817. Likely program:
- 10.00--10.45 Szumi Xie: Tutorial on filling squares in Cubical Agda. Agda file
- 10.45--11.30 András Kovács: Yoneda LF. Digital whiteboard
- 11.30--12.15 Márk Széles: Introduction to string diagrams for probability. Slides
- 12.15--15.00 lunch at Science Park Étterem, then coffee at TTK Étterem
- 15.00--15.45 Bálint Kocsis: Complete Test Suites for Automata in Monoidal Closed Categories. Digital whiteboard
- 15.45--16.30 Péter Diviánszky: Bidirectional parsing of Agda-like syntax. Slides
2024-12-09 Awodey book 4b Groups and categories (Viktor)
2024-12-02 Awodey book 4a Groups and categories (Viktor). Photos
2024-11-25 Awodey book 3c Duality (Ádám). Photos
2024-11-18 Awodey book 3b Duality (Ádám). Photos
2024-11-11 Awodey book 3a Duality (Ádám). Photos
2024-11-04 Awodey book 2 Abstract structures (Gergő). Photos
2024-10-21 Awodey book 1b Categories (Ambrus). Photos
2024-10-14 Awodey book 1a Categories (Peti). Photos
2024-10-07 Ambrus Kaposi. SOGAT -> GAT translation. Photos | Paper
2024-09-30 Balázs Kőműves. Succinct proofs of arbitrary computations. Slides
2024-09-23 Szumi Xie. Type theory with implicit complexity. Photos
2024-09-16 Zoltán Kocsis. The Probability of Excluded Middle. Abstract | Photos | Paper
2024-09-09 Ambrus Kaposi. CCC és STLC ekvivalenciája. Photos
2024-09-02 Loïc Pujet. A new universe construction for setoids. Digital whiteboard
2024-08-26 René Gazzari. A New Approach to Constructive Equality. Digital whiteboard
2024-07-24 András Kovács. Stream fusion using two-level type theory. Paper | Photo
2024-07-01 Lorenzo Sauras. On the representation of Kalmár functions as arithmetic terms. Digital whiteboard
2024-06-24 Jacob Neumann. Directed type theory. Digital whiteboard
2024-06-17 Thorsten Altenkirch. Higher containers. Digital whiteboard
2024-06-10 (no seminar, TYPES in Copenhagen)
2024-06-03 Pre-TYPES talks.
- Viktor Bense: Strict syntax of type theory via alpha-normalisation
- Ambrus Kaposi: Internal relational parametricity, without an interval
- Szumi Xie: Type theory in type theory using single substitutions
2024-05-27
2024-05-23 Gergely Székely. Logic for relativity theory. Slides
2024-05-16 Ambrus Kaposi. Single substitutions. Digital whiteboard
2024-05-09 Ambrus Kaposi. Metaprogramming through two-level type theory. Digital whiteboard
2024-05-02 Szumi Xie. Normalisation by evaluation vs. big-step normalisation. Agda file
2024-04-25 Bálint Kocsis. Normalisation and gluing. Slides
2024-04-18 Gábor Sági. A quick survey of the basics of algebraic logic -- part 1. Slides
Zalán Molnár. A quick survey of the basics of algebraic logic -- part 2. Slides
2024-04-11 (no seminar, MGS)
2024-03-21 Szumi Xie. Optics in Haskell. Digital whiteboard
2024-03-14 Rafaël Bocquet. The cubical set model using internal techniques. Digital whiteboard
2024-03-07 Szumi Xie. SOGAT -> GAT translation. Digital whiteboard | Paper
2024-02-29 no seminar, at 17.30, Rafaël gives HoTTeST seminar, see here.
2024-02-22 Balázs Kőműves. Ellipses and elliptic curves, what's the deal. Slides
2024-02-15 Discussing schedule of seminars and W-types. Digital whiteboard
2024-01-12 World Logic Day in Pécs
2024-01-10 January type theory workshop. Location: D-1-817. Program:
- 10.15--11.00 Rafael Bocquet: Normalisation for a theory with definitional groups Digital whiteboard
- 11.00--11.45 Viktor Bense: How to write Agda code
- 12.15--14.00 lunch at Science Park Étterem
- 14.00--14.45 Ambrus Kaposi: Internal parametricity, without an interval Paper
- 14.45--15.30 Márk Széles: Towards a probabilistic logic with updating Digital whiteboard
- 15.30--15.45 Szumi Xie: Normalisation for a type theory with impredicative Set Digital whiteboard
2023-12-14 PhD defence of Richárd Szalay, room D-2-214
2023-12-07 Presheaf models, law of excluded middle, prefascist sets
2023-11-30 QIIRTs
2023-11-23 Csimma Viktor. Creating an agda2hs-compatible representation of Krebbers–Spitters reals
2023-11-16 Kovács András. TBA
2023-11-09 Riehl book Section 1.4
2023-10-19 Riehl book Section 1.3
2023-09-28 Riehl book Section 1.2
2023-09-21 Riehl book Section 1.1
2023-09-14 Substitution normal forms. Photo
2023-08-23 Márk Széles. A synthetic approach to probability theory. Digital whiteboard
2023-08-16 Ambrus Kaposi. A type theory with internal parametricity. Photo
2023-08-02
2023-07-12 Ambrus Kaposi. Internal parametrcity, without an interval. Photos | Paper
2023-06-28 FSCD preparation talks Paper 1 | Paper 2 | Digital whiteboard
2023-06-21 Thorsten Altenkirch. Bushes and higher containers. Digital whiteboard
2023-06-14 (no seminar, TYPES in Valencia)
2023-06-07 Canonicity proofs for type theory
2023-05-31 Random discussion
2023-05-24 Yorgo Chamoun. On automata theory
2023-05-17 András Cubical test presentation
2023-05-10
2023-05-03 Diviánszky Péter. A type checker for dependent types
2023-04-19 Mátyás Szokoli. Erlang type inference
2023-04-12 Rafaël Bocquet. Sconing test presentation (half an hour)
2023-04-05 András: II.15. Image factorisation Book
2023-03-29 András: II.14. Propositional Truncation Book
2023-03-22 Ambrus: II.13. Funext Book
2023-03-16 Rafaël: II.12. H-levels Digital whiteboard | Book
2023-03-09 András: II.11. Fundamental theorem of Id type Book
2023-03-02 Ambrus. Single substitution calculus
2023-02-23 Rafaël: II.10. Contractible types Book
2023-02-16 Borka: II.9. Equivalence Book
2023-02-09 Higher equalities Digital whiteboard
Egbert Rijke's book, section I.6 Book
2023-02-02 Plan talks at department workshop
2023-01-26 Egbert Rijke's book, section I.5 Digital whiteboard | Book
2023-01-19 Plans for next semester; propositional proof irrelevance for setoid hell QIITs. Digital whiteboard
2023-01-12 András Kovács. Theory of Signatures for higher inductive inductive recursive types. Photos
2023-01-05 Type theory and first order logic as second order generalised algebraic theories. Photo
2022-12-15 Ambrus Kaposi. Reedy fibrant presheaves
2022-12-09 András Kovács PhD defence
2022-12-05 Discussion about setoid type theory metatheory
2022-11-28 Rafaël Bocquet. Relative induction principles
2022-11-21 Balázs Kőműves. Introduction to Zero-Knowledge Proof systems. Slides
2022-11-14 Tamás Végh. Combinators. Formalisation
2022-11-07 Rafaël Bocquet. External univalence
2022-10-28 SeTT Implementation Day. Github project
2022-10-24 András Kovács. Theory of Signatures. Photo
2022-10-17 Marcin Grzybowski. Visualizing compositions from Cubical Agda | Github account
2022-10-10 Ambrus Kaposi. QIIRTs. Notes | Agda file
2022-10-03 Rafaël Bocquet. W-Types. Notes
2022-09-26 István Donkó. Introduction to CwF with Bool,Π
2022-09-19 Topics for the semester. Notes
2022-09-12 Canonicity for type theory. Notes
2022-09-06 SeTT implementation day. Github project
2022-08-29 SeTT implementation day. Github project
2022-08-17 François-René ÐVB Rideau. Object Orientation, Functionally; First class implementations. Paper | Paper sources and video | Faré's blog | Faré's thesis draft
2022-08-01 SeTT implementation day. Github project
2022-07-18 András Kovács. Staging and partially static data. Digital whiteboard
2022-07-15 SeTT implementation day Github project
2022-07-08 SeTT implementation day Github project
2022-06-13 Ambrus Kaposi. Strictification of a category. Digital whiteboard
2022-05-30 Studying category theory. Thorsten's notes and slides
2022-05-23 Meeting with András Simon and Zoltán Molnár at BME
2022-05-16 Thorsten Altenkirch. The axiom of choice and variations. Photo
2022-05-09 Ambrus Kaposi. Combinator logic and lambda calculus.
2022-05-02 Studying category theory. Thorsten's notes and slides
2022-04-11 Studying category theory. Thorsten's notes and slides
2022-03-28
2022-03-21 List of possible topics. The axiom of choice in type theory. Photos
2022-03-14
2022-03-07 Ambrus Kaposi. Higher observational type theory. Photos
2022-03-02 Ulrik Buchholtz (joint meeting with the Nottingham type theory café)
2022-02-28
2022-02-21 Ambrus Kaposi. Mutual definition of presheaves and type theory. Notes
2022-02-14 Thorsten Altenkirch. Higher order containers. Photos
2022-02-07 András Kovács. Cubical type theory
2022-01-31 András Kovács. More on staged compilation
2022-01-26 Rafaël Bocquet. Strictification of weakly stable type-theoretic structures using generic contexts. Notes | Paper (joint meeting with the Nottingham type theory café)
2022-01-24 András Kovács. Staged compilation and two level type theory. Notes
2022-01-10 Discussion (online)
2021-12-06 Study this
2021-12-01 Thorsten Altenkirch. Münchhausen type theory. Notes (joint meeting with the Nottingham type theory café)
2021-11-29 Péter Bereczky. Core Erlang formalisation Github project
2021-11-08 Ambrus Kaposi. Inductive types: injectivity, disjointness of constructors, decidability of equality. Photos
Rafaël Bocquet. A generalisation of the local usiverses method. Photos
2021-10-27 Ambrus Kaposi. Relative displayed models. Notes (joint meeting with the Nottingham type theory café)
2021-10-25 Péter Diviánszky. A dependently typed assembly language. Website
2021-10-18 Guilherme Silva. Formalising Bitcoin in Agda. Github repo, another Github repo
2021-09-27 András Kovács. Simply typed CwF. Photos
2021-09-20 Rafaël Bocquet. Coherence theorems for type theory
2021-09-13 Ambrus Kaposi. Normalisation for SK combinator calculus. Photos | Notes
2021-09-06 Discussion of topics for this semester. Ambrus Kaposi. Levels of abstraction when defining programming languages. Photos
2021-06-18 Developments in Computer Science conference, session on type theory:
- Invited talk. Nicolai Kraus. Wellfounded and Extensional Ordinals in Homotopy Type Theory. Slides
- Rafaël Bocquet. Univalent transport in type theory. Slides
- István Donkó. Properties of Setoid Type Theory. Slides
- András Kovács. Staged Compilation and Generativity. Notes
- Szumi Xie. A model of type theory supporting quotient inductive-inductive types. Slides
2021-06-09 Thorsten Altenkirch. A telescope calculus. Notes
2021-06-02
2021-05-26 Nicolai Kraus. Riehl-Shulman type theory for infinity categories. Notes
2021-05-19 Discussing topics for Agda Implementors Meeting. List
2021-05-12
2021-05-05 Egbert Rijke. New universal properties of the truncations
2021-04-28 Discussion on e.g. free algebraic structures. Notes
2021-04-21 Hugo Moeneclaey. Parametricity and Semi-Cubical Types
2021-04-14
2021-04-07 Thorsten Altenkirch. The CwF of containers
2021-03-31 Fredrik Nordvall Forsberg. Quantitative type theory. Notes
2021-03-24 Filippo Sestini. Reducing infinitary inductive-inductive types to inductive types.
2021-03-17
2021-03-10 Rafaël Bocquet. Induction principles for type theories, internally to presheaf categories. Notes | Paper
2021-03-03 András Kovács. Universes. Notes | Paper
2021-02-15 Thorsten Altenkirch. A new theory of signatures for describing inductive-inductive types.
2021-02-08 Brandon Hewer. An efficient universe of finite sets in Agda. Github repo
2021-02-01 New ideas about QIITs. Whiteboard
2021-01-25 Rafaël Bocquet. Metatheoretic proofs internally to presheaf categories Notes
2021-01-11 András Kovács. What is a type theory with inductive-inductive types? Notes
2020-12-10 András Kovács. Substitutions, renamings, weakenings
2020-12-08 Rafaël Bocquet. TT intro 13 groupoid model. Video | Notes
2020-12-01 András Kovács. TT intro 12 normalisation. Video | Notes
2020-11-24 Ambrus Kaposi. TT intro 11 metatheoretic properties. Video | Notes
2020-11-19 Gregory Morse. Snake in Agda. Github repo
2020-11-17 Rafaël Bocquet. TT intro 10 two level type theory. Video | Notes
2020-11-10 András Kovács. TT intro 09 Yoneda embedding. Video | Notes
2020-11-05 András Kovács. Universes
2020-11-03 Ambrus Kaposi. TT intro 08 presheaf models. Video | Notes | Extra notes
2020-10-27 Ambrus Kaposi. TT intro 07 Exercises
2020-10-20 Rafaël Bocquet. TT intro 06 family model. Video | Notes
2020-10-15 András Kovács. Setoid type theory. Notes
2020-10-13 András Kovács. TT intro 05 identity types. Video | Notes
2020-10-06 Ambrus Kaposi. TT intro 04 universes. Video | Notes
2020-10-01 Rafaël Bocquet. A variant of Brunerie's type theoretic definition of ∞-groupoids. Notes
2020-09-29 Rafaël Bocquet. TT intro 03 standard model. Video | Notes
2020-09-24 András Kovács. Setoid type theory implementation. Notes
2020-09-22 András Kovács. TT intro 02 cwf. Video | Notes
2020-09-17 András Kovács. A game semantics of MLTT. Formalisation
2020-09-15 Ambrus Kaposi. TT intro 01 basics of dependent type theory. Video | Notes
2020-07-28 András Kovács. Staged compilation and two-level type theory. Implementation
2020-07-07 Dániel A. Nagy. Seedling, A Programming Language for Everyone and Everything. Github repo
2020-06-30 Zoltán A. Kocsis. Internal set theory. Notes txt | Notes png | PhD thesis | Agda code for the thesis
2020-06-23 András Kovács. The container model of type theory. Agda file
Ambrus Kaposi. Reduction of inductive-inductive types to indexed inductive types. Agda file
2020-06-16 Thorsten Altenkirch. Integers as a higher inductive type. Paper | LICS talk
Paolo Capriotti. Dimensions in physics
2020-06-09 Logic in Agda. Agda repo
2020-06-02 Discussion on random topics
2020-05-26 Paolo Capriotti. The simplicial set model of HoTT. Notes
2020-05-19 András Kovács. Elaboration with first-class implicit function types. Paper | Notes
2020-05-12 Discussion on logical predicates/relations and simplicial/cubical type theories. Notes
2020-05-04 Rafaël Bocquet. Presentation of the paper "Multi-modal type theory". Notes | Paper1 | Paper2
2020-04-28 Thorsten Altenkirch. Higher categories in homotopy type theory. Notes
2020-04-21 Rafaël Bocquet. Presentation of the paper "A Higher Structure Identity Principle" by Ahrens et al. Notes | Paper
2020-04-14 András Kovács. An implementation of setoid type theory. Github repo
2020-04-07 Rafaël Bocquet. Conservativity of type theory theory with strict computation rules over weak type theory. Notes
2020-03-31 Péter Diviánszky. A very fast lambda calculus interpreter based on combinatory logic. Haskell implementation
2020-03-24 Christian Sattler. Strict presheaf models. Paper 1 | Paper 2
2020-03-17 Post-TYPES talks.
- Nicolai Kraus. An Induction Principle for Cycles. Abstract | Slides
- Filippo Sestini. Constructing a universe for the setoid model. Abstract
- Rafaël Bocquet. Metatheoretic proofs internally to presheaf categories. Abstract
2020-03-10 Ambrus Kaposi. A point-free definition of hProp and using it to define the setoid model. Photos
2020-03-03 András Kovács. Evaluation efficiency issues in cubical type theory
2020-02-18 Pre-TYPES talks.
- András Kovács. Generalizations of Quotient Inductive-Inductive Types. Photos | Abstract
- Szumi Xie. A model of type theory with QIITs. Abstract
- Ambrus Kaposi. Shallow embedding of type theory is morally correct. Abstract
- Rafaël Bocquet. Metatheoretic proofs internally to presheaf categories. Abstract
2020-02-11 András Kovács. Type checking. Photos
2020-02-03 Christian Sattler. Filtered colimits.
2020-01-27 Ádám Révész. LambdaKube: kubernetes based cloud native functional programming language design and implementation with tools.
2020-01-20
2020-01-13 Ambrus Kaposi. Substitution laws for free! Signatures for type theories. Photos
2020-01-07 Paolo Capriotti. Sketches and inductive types.
2019-12-16 András Kovács. Introduction to type theory for proof theorists (iii). Agda file
2019-12-09 Ambrus Kaposi. Introduction to type theory for proof theorists (ii). Photos
2019-12-02 Derivation of Frobenius J from J. Formalisation
2019-11-25 Ambrus Kaposi. Introduction to type theory for proof theorists (i). Photos | Simple type theory | Dependent type theory
2019-11-18 Ambrus Kaposi. Presheaf models, showing that LEM is not provable. Photos
2019-11-11 Rafaël Bocquet. Slice models of type theory. Photos
2019-11-04 András Kovács. Large numbers in type theory. Photos
2019-10-28 Discussing "Implementing a Modal Dependent Type Theory". Paper
2019-10-21 Rafaël Bocquet. Nonstandard models of type theory. Photos
2019-10-14 Discussing "A Language Feature to Unbundle Data at Will". Paper | Website
2019-10-07 András Kovács. Type inference. Github repo
2019-09-30 Discussion about ICFP experiences
2019-09-23 Secret Information. Characterisation of definability for dependent type theory.
2019-09-16 Revisiting definability for simple type theory. Photos
2019-09-09 Nicolai Kraus. Higher type theory
2019-09-02 Ambrus Kaposi. Transformations between classes of inductive types. Photos
András Kovács. Extra constructions on QIITs: coproducts, natural number objects, etc. Photos | Paper on basic constructions on QIITs
2019-08-12 Discussion on higher semi type theory. Photos
2019-07-29 Ambrus Kaposi. All inductive-inductive types (IITs) are reducible to two-sorted IITs, this also gives sort equalities. Photos
2019-07-22 András Kovács. A failed construction of a coherent syntax. Photos
Ambrus Kaposi. Type theory without identities is enough. Photos
2019-07-15 Rafaël Bocquet. Coherence for two-level type theory. Photos
2019-07-08 Thorsten Altenkirch. Directed type theory. Photos
2019-07-01 Joseph Helfer. First order homotopical logic
2019-06-24 Ambrus Kaposi. Setoidification of setoid type theory is injective. Photos
2019-06-17 Mihály Makkai. Generalised sketches. Paper part 1, part 2, part 3
2019-06-03 Mihály Makkai. Generalised sketches. Paper part 1, part 2, part 3
2019-05-27 Dániel Lukács. Linear temporal Logic. Photos
2019-05-20 András Kovács. The category of algebras for single sorted algebraic theories without equalities. Photos
2019-05-13 Nicolai Kraus. Deep and shallow embeddings of groups. Photos
2019-05-06 Studying "Call-by-need is clairvoyant call-by-value" by Hackett and Hutton. Paper
2019-04-29 Ambrus Kaposi. Shallow embedding is morally correct. Photos | Paper
2019-04-15 Studying Mike Shulman's "Linear logic for constructive mathematics". Photos | Paper
2019-04-08 Studying Mike Shulman's "Linear logic for constructive mathematics". Paper
2019-04-01 Thorsten's directed type theory. Photos | Some slides
2019-03-25 András Kovács. Initiality project. Photos
2019-03-18 Open discussion including Péter Diviánszky
2019-03-11 Simon Boulier. Template Coq
2019-03-04 Gábor Lehel. Rust for Haskellers. Slides | Source of slides
2019-02-25 Ambrus Kaposi. Shallow embedding is morally correct. Photos
2019-02-18 Studying Conor McBride's Outrageous but Meaningful Coincidences paper. Photos | Paper
2019-02-11 Ambrus Kaposi. Setoid model -> translation -> type theory. Canonicity from gluing. Photos | Setoid type theory paper | Gluing paper
2019-02-04 Ambrus Kaposi. Introduction to the algebraic syntax of type theory. Photos
2019-01-28 Dávid Németh. Introduction to the K framework. Zsolt Tabi. Agile methods.
2019-01-21 Jakob von Raumer. Path Spaces of Higher Inductive Types in Homotopy Type Theory. Photos | Paper
2019-01-14 Ambrus Kaposi. Algebraic programming language theory. Photos | Slides for another talk on the same topic
2019-01-07 Who did what in the Christmas break. Photos
2018-12-17 Ambrus Kaposi. Setoid type theory. Photos | Paper
2018-12-10 András Kovács. Efficient type checker for dependent types, part 2. GitHub repo
2018-12-03 András Kovács. Efficient type checker for dependent types, part 1. GitHub repo
2018-11-26 Finite models of type theory. Some formalisation
2018-11-19 Ambrus Kaposi. Syntax of type theory and a trivial model. Photos | Leaflet | Source code of leaflet
2018-11-12 Péter Diviánszky. What is a composable interactive program? GitHub repo
2018-11-05 Péter Diviánszky. What is an interactive program? Photos | GitHub repo
2018-10-29 Ambrus Kaposi. Setoid type theory. Photos | Paper
2018-10-15 Ambrus Kaposi. Canonicity for simple type theory. Photos
2018-10-08 Gergő Érdi. Generic Description of Well-Scoped, Well-Typed Syntaxes. Paper | GitHub repo
2018-10-01 Recursion, induction, injectivity and disjointness of constructors. Photos | Source code
2018-09-24 András Kovács. Agda intro to haskellers. Source code
2018-09-17 Universe levels, sets as trees, Russell paradox, HITs. Photos
2018-09-10 Intro to Lambda calculus and variants of type theory. Photos
2018-09-03 List of possible topics, interaction nets. Photos
2018-08-28 Thorsten Altenkirch. Coherent type theory
2018-06-26 Constructing QIITs. Photos | Paper | Bitbucket repo
2018-04-13 Intrinsic syntax of type theory with generalise. Photos
2018-02-27 András Kovács. Closure conversion for dependent types. Photos | TYPES slides | TYPES abstract
2018-02-13 András Kovács. Inductive types from functors given by I-K-etc. combinators. Photos
2017-12-11 Elimination principles for inductive types with negative constructors. Photos
2017-12-04 András Kovács. Elaboration. Photos
2017-11-27 Quotient by group action. Photos
2017-11-20 Algebra morphisms for natural numbers, groups, logic, type theory.. Photos
2017-10-23 A syntax for inductive-inductive types. Photos
2017-10-02 The meta-metatheory of inductive types. Photos
2017-09-25 Type theory intro. Photos
2017-09-11 András Kovács. Generalised generic trie. Photos
2017-08-01 Circle, propositional truncation. There are no coproducts in lazy languages. Photos
2017-06-13 Conversion checking for type theory (Coquand's algorithm). Photos
2017-06-06 Equality reflection implies UIP and other stuff. Photos
2017-05-29--06-01 We organised the 23rd International Conference on Types for Proofs and Programs (TYPES 2017) in Budapest
2017-05-22 Deriving types of elimination principles. Photo
2017-05-16 Eliminator from recursor and uniqueness for natural numbers. Conversion checking for type theory. Photos
2017-05-02 STRef. Fibrational setoid type theory. Photos
2017-04-04 Deriving types of elimination principles. Photos
2017-03-28 Deriving types of elimination principles. Photos
2017-03-21 Deriving types of elimination principles. Photos
2017-03-14 Deriving types of elimination principles. Photos
2017-03-07 Type checking for dependent types producing intrinsic syntax. Photos
2017-03-02 Deriving types of elimination principles. Photos
2017-02-21 Induction-induction, induction-recursion, initial algebra semantics of inductive types, construcing initial algebra using quotients. Photos
2017-02-14 Constructing initial algebras using quotients. Photos
2017-02-07 Minimal cubical type theory. Photos
2017-01-24 Logical predicates with universes a la Russell or Tarski? Category with families. Photos
2017-01-17 External and internal parametricity, cubes. Photos
2017-01-03 Eliminator for nested lists. Deriving types of elimination principles. Photos
2016-12-20 Logical predicates. Photos
2016-12-13 András Kovács. Pattern unification. Photos
2016-12-06 András Kovács. Unification. Photos
2016-11-15 Ambrus Kaposi. Categories, functors from positive and negative type expressions. At Bolyai Kollégium. Photos
2016-11-08 Ambrus Kaposi. Category theory and computer science. At Bolyai Kollégium. Photos
2016-10-18 Péter Diviánszky. A calculus for implicit arguments. Photos
2016-10-13 Ambrus Kaposi. W-types. Photos
2016-10-03 Ambrus Kaposi. Normalisation for simple type theory. Photos
2016-09-20 Yoneda lemma. Categorical gluing. Operational semantics for lazy evaluation. Photos
2016-09-12 Studying the CCHM paper on cubical type theory. Photos | Paper
2016-09-05 Studying the CCHM paper on cubical type theory. Photos | Paper
2016-09-01 Studying the CCHM paper on cubical type theory. Photos | Paper
2016-08-22 Studying the CCHM paper on cubical type theory. Photos | Paper
2016-07-04 András Kovács. Push-enter, eval-apply. Photos
2016-06-27 Péter Diviánszky. Implementing functional languages. Photos
2016-06-13 András Kovács. Presentation of "Unifiers as Equivalences" paper by Cockx, Devriese, Piessens. Photos | Paper
2016-06-06 Péter Diviánszky. An operational semantics for dependent types. Photos
2016-05-16 Ambrus Kaposi. Intrinsic syntac of simple type theory, standard model, normal forms. Photos
2016-05-09 Balázs Kőműves. Topology and type theory. Photos
2016-05-02 Balázs Kőműves. Topology. Photos
2016-04-25 Ambrus Kaposi. Quotient types, intrinsic syntax for type theory. Photos
2016-04-18 List of possible topics, simple type theory, intrinsic syntax. Photos
2016-04-10 Ambrus Kaposi. Logical relations and identity types.

Teaching

We are responsible for the following courses at the Faculty of Informatics:

Theses and publications

PhD theses defended in the type theory group at ELTE:

HOTT ERC project

Funding Acknowledgement: Our research is generously supported by the HOTT ERC grant 101170308.

The goal of this project is to develop Higher Observational Type Theory (HOTT), a new version of homotopy type theory (HoTT) featuring definitional univalence. The starting point is a theory of internal parametricity (an indexed version) which supports a baby identity type which is reflexive and a congruence, but not symmetric or transitive. The goal is to extend this to a proper identity type supporting transport. See also the series of talks by Michael Shulman (slides 1, 2, 3, videos 1, 2, 3) and his experimental proof assistant Narya.