-
Formalizing type theory through transport hell
SSTT
2026, Ljubljana
abstract ·
slides
-
Eliminating finitary inductive-inductive types without K
TYPES
2026, Gothenburg
abstract ·
slides
-
The groupoid-syntax of type theory is a set
HoTTEST
(2026), online
slides ·
video
-
The conatural numbers form an exponential commutative semiring
TyDe
2025, Singapore
slides ·
video
-
Type theory with single substitutions
LFMTP
2025, Birmingham
slides
-
Conatural numbers in Cubical Agda
Agda Implementors’ Meeting XL
(2025), Budapest
Agda file 1
·
Agda file 2
-
Second-order generalized algebraic theories (logic edition)
World Logic Day 2025, Budapest
abstract ·
slides
-
Second-order generalised algebraic theories (lightning edition)
SPLV
2024
lightning talk, Glasgow
slides
-
Second-order generalised algebraic theories: signatures and
first-order semantics
FSCD
2024, Tallinn
slides
-
Type theory in type theory using single substitutions
TYPES
2024, Copenhagen
abstract ·
slides
-
A model of type theory supporting quotient inductive-inductive types
Developments in Computer Science
(2021), Budapest (online)
abstract ·
slides
-
A model of type theory with quotient inductive-inductive types
TYPES
2020, Turin (cancelled)
abstract ·
slides