Accepted Contributions

Book of Abstracts


List of Contributions

TitleAuthorsSession
A Gradual Intersection Typed CalculusPedro Ângelo and Mário FloridoComputation and Intersection Types
Intersection Types for a Computational Lambda-Calculus with Global StateUgo De’Liguoro and Riccardo TregliaComputation and Intersection Types
The syntactic tale of the oracle and the treesMartin Baillon and Pierre-Marie PédrotComputation and Intersection Types
Novel rules of β-conversion in partial type theoryJiří Raclavský and Petr KuchyňkaComputation and Intersection Types
Quotient inductive-inductive types in the setoid modelAmbrus Kaposi and Zongpu XieInductive Types
Eliminating Infinitary Induction-inductionFilippo Sestini and Thorsten AltenkirchInductive Types
Simulating large eliminations in CedilleChristopher Jenkins, Andrew Marmaduke and Aaron StumpInductive Types
A container model of type theoryThorsten Altenkirch and Ambrus KaposiLogical and Semantic Principles
Quantitative polynomial functorsGeorgi Nakov and Fredrik Nordvall ForsbergLogical and Semantic Principles
Shape-irrelevant reflection: Terminating extensional type theoryThéo WinterhalterLogical and Semantic Principles
On Model-Theoretic Strong Normalization for Truth-Table Natural DeductionAndreas AbelLogical and Semantic Principles
On the logical structure of choice and bar induction principlesNuria Brede and Hugo HerbelinLogical and Semantic Principles
Modalities and Parametric AdjointsDaniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto and Lars BirkedalModal Type Theory
Normalization for multimodal type theoryDaniel GratzerModal Type Theory
Clocked Cubical Type TheoryMagnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg and Andrea VezzosiModal Type Theory
Semantic Analysis of Normalization by Evaluation for Fitch-Style Modal Lambda CalculiNachiappan Valliappan, Fabian Ruch and Carlos Tomé CortiñasModal Type Theory
Interpreting Twisted Cubes as Partially Ordered SpacesGun PinyoModel Theory
B-systems and C-systems are equivalentBenedikt Ahrens, Jacopo Emmenegger, Paige North and Egbert RijkeModel Theory
A finite-dimensional model for affine, linear quantum lambda calculi with general recursionAlejandro Díaz-Caro, Malena Ivnisky, Hernán Melgratti and Benoît ValironModel Theory
Semisimplicial Types in Internal Categories with FamiliesJoshua Chen and Nicolai KrausModel Theory
Types are internal infinity-groupoidsAntoine Allioux, Eric Finster and Matthieu SozeauModel Theory
Syntax for two-level type theoryRoberta Bonacina and Benedikt AhrensNew Type Theories
Using Two-Level Type Theory for Staged CompilationAndrás KovácsNew Type Theories
Native Type TheoryChristian Williams and Michael StayNew Type Theories
Functorial AdaptersConor Mcbride and Fredrik Nordvall ForsbergNew Type Theories
Type theories without contextsAndrej Bauer and Philipp G. HaselwarterNew Type Theories
Equality checking for dependent type theoriesAndrej Bauer and Anja PetkovićProof Assistants Foundations
Family Polymorphism for Proof ExtensibilityAnastasiya Kravchuk-Kirilyuk, Yizhou Zhang and Nada AminProof Assistants Foundations
A Drag-and-Drop Proof TacticBenjamin Werner, Pablo Donato and Pierre-Yves StrubProof Assistants Foundations
A proof assistant for synthetic ∞-categoriesNikolai KudasovProof Assistants Foundations
A Practical Implementation of Twin TypesVíctor López JuanProof Assistants Foundations
Modelling Smart Contracts of Bitcoin in AgdaAnton Setzer and Bogdan Gabriel LazarProof Assistants Applications
The Agda Universal Algebra Library and Birkhoff’s Theorem in Dependent Type TheoryWilliam DeMeoProof Assistants Applications
A Formal Theory of Games of Incomplete InformationHelene Fargier, Érik Martin-Dorel and Pierre Pomeret-CoquotProof Assistants Applications
SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqCarmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hritcu, Kenji Maillard and Bas SpittersProof Assistants Applications
Towards Automation for IrisIke Mulder and Robbert KrebbersProof Assistants Applications
On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional LogicAsta Halkjær From and Jørgen VilladsenProof Theory
Zaionc paradox revisitedPierre LescanneProof Theory
Proof terms for generalized classical natural deductionHerman Geuvers and Tonny HurkensProof Theory
Size-Based Termination for Non-Positive TypesYuta TakahashiRecursion
Constructive Notions of Ordinals in Homotopy Type TheoryNicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie XuRecursion
Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset FunctorNiccolò VeltriRecursion
A Formalisation of Approximation Fixpoint TheoryBart Bogaerts and Luís Cruz-FilipeRecursion
M-types and BisimulationDaniël Otten and Henning BasoldRecursion