TYPES 2024: TYPES 2024

A
Abel, Andreas	Type-Based Termination Checking in Agda
Affeldt, Reynald	Yet another formal theory of probabilities (with an application to random sampling)
Ahman, Danel	Comodule Representations of Second-Order Functionals
Ahrens, Benedikt	The Univalence Maxim and Univalent Double Categories
Alhabardi, Fahad	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
Altenkirch, Thorsten	Internal relational parametricity, without an interval Coherent Categories with Families
B
Baillon, Martin	A zoo of continuity properties in constructive type theory
Barenbaum, Pablo	Useful Evaluation, Quantitatively
Barras, Bruno	Towards a logical framework modulo rewriting and equational theories
Basold, Henning	Harmony in Duality
Bauer, Andrej	Comodule Representations of Second-Order Functionals
Bense, Viktor	Strict syntax of type theory via alpha-normalisation
Birkedal, Lars	A modal deconstruction of Loeb induction
Bradley, Felix	Representing Temporal Operators with Dependent Event Types
Bruni, Alessandro	Yet another formal theory of probabilities (with an application to random sampling)
Brædder, Laura	A formal security analysis of Blockchain voting
Buchholtz, Ulrik	Universes in simplicial type theory
C
Chapman, James	Mechanizing BFT consensus protocols in Agda
Cherubini, Felix	Synthetic Stone duality
Chodarev, Sergej	OnlineProver: A proof assistant for online teaching of formal logic and semantics
Chu, Fernando	A directed homotopy type theory for 1-categories
Cockx, Jesper	A generic translation from case trees to eliminators
Cohen, Liron	Limited Principles of Omniscience in Constructive Type Theory
Coquand, Thierry	Synthetic Stone duality Poset Type Theory
D
da Rocha Paiva, Bruno	Limited Principles of Omniscience in Constructive Type Theory
de Jong, Tom	Constructive Ordinal Exponentiation in Homotopy Type Theory
Dybjer, Peter	Special Session in Memory of Peter Aczel Predicativity of the Mahlo Universe in Type Theory
E
Escot, Lucas	A generic translation from case trees to eliminators
Espírito Santo, José	Faithful interpretations of LJT and LJQ into polarized logic
F
Felicissimo, Thiago	Towards a logical framework modulo rewriting and equational theories
Forster, Yannick	A zoo of continuity properties in constructive type theory Limited Principles of Omniscience in Constructive Type Theory Post’s Problem and the Priority Method in CIC
G
Gambino, Nicola	Logic in Dependent Type Theory
Geerligs, Freek	Synthetic Stone duality
Geuvers, Herman	Normalization of Natural Deduction for Classical Predicate Logic Harmony in Duality
Gratzer, Daniel	A modal deconstruction of Loeb induction Universes in simplicial type theory
Gylterud, Håkon Robbestad	Univalent Material Set Theory: Hierarchies of n-types
Géran, Yoan	A Canonical Form for Universe Levels in Impredicative Type Theory
H
Hansen, Lasse Letager	A formal security analysis of Blockchain voting
Herbelin, Hugo	Size-preserving dependent elimination How much do System T recursors lift to dependent types?
Huang, Yulong	Towards Quantitative Inductive Families
Hurkens, Tonny	Normalization of Natural Deduction for Classical Predicate Logic
Hutzler, Matthias	Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues
Höfer, Jonas	Poset Type Theory
J
Jaskelioff, Mauro	Mechanizing BFT consensus protocols in Agda
Joram, Philipp	Comparing Quotient- and Symmetric Containers
K
Kaposi, Ambrus	Internal relational parametricity, without an interval Strict syntax of type theory via alpha-normalisation Coherent Categories with Families Type theory in type theory using single substitutions
Kesner, Delia	Useful Evaluation, Quantitatively
Kirst, Dominik	The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem Limited Principles of Omniscience in Constructive Type Theory Post’s Problem and the Priority Method in CIC
Kovács, András	Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time
Kraus, Nicolai	Constructive Ordinal Exponentiation in Homotopy Type Theory
Krishnaswami, Neel	Implementing Observational Equality with Normalisation by Evaluation
Kristensen, Joachim Tilsted	OnlineProver: A proof assistant for online teaching of formal logic and semantics Looking Back: A Probabilistic Inverse Perspective on Test Generation
Kupke, Clemens	Extensional Finite Sets and Multisets in Type Theory
L
Larchey-Wendling, Dominique	Quasi Morphisms for Almost Full Relations
Larsen, Ken Friis	Proof and Consequences: Separating Construction and Checking of eBPF Loops
Lee, Sori	Identity types in predicate logic
Lennon-Bertrand, Meven	Implementing Observational Equality with Normalisation by Evaluation
Lieverse, Kayleigh	A generic translation from case trees to eliminators
Ljungström, Axel	A Constructive Cellular Approximation Theorem in HoTT Revisiting the Steenrod Squares in HoTT
Luo, Zhaohui	Representing Temporal Operators with Dependent Event Types
M
Mahboubi, Assia	A zoo of continuity properties in constructive type theory
Maillard, Kenji	Splitting Booleans with Normalization-by-Evaluation
Mangel, Éléonore	A directed homotopy type theory for 1-categories
Mathiesen, Mikkel Kragh	Proof and Consequences: Separating Construction and Checking of eBPF Loops
Matthes, Ralph	Faithful interpretations of LJT and LJQ into polarized logic
Melkonian, Orestis	Mechanizing BFT consensus protocols in Agda
Milicich, Mariana	Useful Evaluation, Quantitatively
Moeneclaey, Hugo	Synthetic Stone duality
N
Neumann, Jacob	Updates on Paranatural Category Theory
Nielsen, Eske Hoy	A formal security analysis of Blockchain voting
Nisht, Kanstantsin	Type-Based Termination Checking in Agda
Nordvall Forsberg, Fredrik	Constructive Ordinal Exponentiation in Homotopy Type Theory Extensional Finite Sets and Multisets in Type Theory
North, Paige Randall	The Univalence Maxim and Univalent Double Categories A directed homotopy type theory for 1-categories
Novotný, Samuel	OnlineProver: A proof assistant for online teaching of formal logic and semantics
O
Otten, Daniël	Semantics of Axiomatic Type Theory
P
Perháč, Ján	OnlineProver: A proof assistant for online teaching of formal logic and semantics
Pientka, Brigitte	Cocon: A Type-Theoretic Framework for Meta-Programming
Pinto, Luís	Faithful interpretations of LJT and LJQ into polarized logic
Piquerez, Matthieu	A zoo of continuity properties in constructive type theory
Pujet, Loïc	A Constructive Cellular Approximation Theorem in HoTT
Pédrot, Pierre-Marie	A zoo of continuity properties in constructive type theory “Proofs are programs” in MLTT
R
Rahli, Vincent	Limited Principles of Omniscience in Constructive Type Theory
Rasekh, Nima	The Univalence Maxim and Univalent Double Categories
Rathjen, Michael	On Relating Type Theories and Set Theories
Reinhard, Tobias	Looking Back: A Probabilistic Inverse Perspective on Test Generation
Rijke, Egbert	Concrete Univalent Mathematics
Ringer, Talia	Bridging Neural and Symbolic Proof Automation
Rossie, Jon	Mechanizing BFT consensus protocols in Agda
Roux, Pierre	Yet another formal theory of probabilities (with an application to random sampling)
S
Saikawa, Takafumi	Yet another formal theory of probabilities (with an application to random sampling)
Setzer, Anton	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness Predicativity of the Mahlo Universe in Type Theory
Shturmov, Oleks	OnlineProver: A proof assistant for online teaching of formal logic and semantics
Shulman, Michael	Internal relational parametricity, without an interval
Sidorenco, Nikolaj	A formal security analysis of Blockchain voting
Sirman, Matthew	Implementing Observational Equality with Normalisation by Evaluation
Spadetto, Matteo	Semantics of Axiomatic Type Theory
Speight, Sam	Partial Combinatory Algebras for Intensional Type Theory
Spitters, Bas	A formal security analysis of Blockchain voting
Steingartner, William	OnlineProver: A proof assistant for online teaching of formal logic and semantics
Stenholm, Elisabeth	Univalent Material Set Theory: Hierarchies of n-types
Swan, Andrew	Oracle modalities
T
Takahashi, Yuta	Large Universe Construction by Indexed Induction-Recursion in Agda
Thomsen, Michael Kirkedal	OnlineProver: A proof assistant for online teaching of formal logic and semantics Looking Back: A Probabilistic Inverse Perspective on Test Generation
Tveito, Lars	OnlineProver: A proof assistant for online teaching of formal logic and semantics
V
Vadgaard, Lars-Bo Husted	OnlineProver: A proof assistant for online teaching of formal logic and semantics
van den Berg, Benno	Recent progress in the theory of effective Kan fibrations in simplicial sets
van der Weide, Niels	The Univalence Maxim and Univalent Double Categories The Internal Language of Univalent Categories
Veltri, Niccolò	Comparing Quotient- and Symmetric Containers
W
Watters, Sean	Extensional Finite Sets and Multisets in Type Theory
Weinberger, Jonathan	Universes in simplicial type theory
Winterhalter, Théo	Towards a logical framework modulo rewriting and equational theories
Wullaert, Kobe	A formal study of the Rezk completion
Wärn, David	Revisiting the Steenrod Squares in HoTT
X
Xie, Szumi	Strict syntax of type theory via alpha-normalisation Type theory in type theory using single substitutions
Xu, Chuangjie	Constructive Ordinal Exponentiation in Homotopy Type Theory
Y
Yallop, Jeremy	Towards Quantitative Inductive Families
Z
Zeng, Haoyi	The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem Post’s Problem and the Priority Method in CIC
Zeuner, Max	Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues
Ü
Üsküplü, Elif	Internal relational parametricity, without an interval

Disclaimer | Powered by EasyChair Smart Program