Start TimeTitleAuthors11:30Modelling Smart Contracts of Bitcoin in AgdaAnton Setzer and Bogdan Gabriel Lazar11:45The Agda Universal Algebra Library and Birkhoff’s Theorem in Dependent Type TheoryWilliam DeMeo12:00A Formal Theory of Games of Incomplete InformationHelene Fargier, Érik Martin-Dorel and Pierre Pomeret-Coquot12:10SSProve: 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 Spitters12:20Towards Automation for IrisIke Mulder and Robbert Krebbers

Towards Automation for Iris

1 file(s) 227.53 KB Download

The Agda Universal Algebra Library and Birkhoff’s Theorem in Dependent Type Theory

1 file(s) 156.58 KB Download

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

1 file(s) 286.30 KB Semantic Analysis of Normalization by Evaluation for Fitch-Style Modal Lambda Calculi

1 file(s) 288.74 KB Download

Normalization for multimodal type theory

1 file(s) 231.94 KB Download

Modalities and Parametric Adjoints

1 file(s) 220.19 KB Download

Clocked Cubical Type Theory

1 file(s) 338.62 KB Download

Proof Assistants Foundations

Start TimeTitleAuthors11:30Equality checking for dependent type theoriesAndrej Bauer and Anja Petković11:40Family Polymorphism for Proof ExtensibilityAnastasiya Kravchuk-Kirilyuk, Yizhou Zhang and Nada Amin11:55A Drag-and-Drop Proof TacticBenjamin Werner, Pablo Donato and Pierre-Yves Strub12:10A proof assistant for synthetic ∞-categoriesNikolai Kudasov12:20A Practical Implementation of Twin TypesVíctor López Juan

Family Polymorphism for Proof Extensibility

1 file(s) 172.08 KB Download

Equality checking for dependent type theories

1 file(s) 280.50 KB Download

A proof assistant for synthetic ∞-categories

1 file(s) 247.29 KB Download

A Practical Implementation of Twin Types

1 file(s) 69.24 KB Download

A drag-and-drop proof tactic

…

Proof Theory

Start TimeTitleAuthors13:30On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional LogicAsta Halkjær From and Jørgen Villadsen13:45Zaionc paradox revisitedPierre Lescanne14:00Proof terms for generalized classical natural deductionHerman Geuvers and Tonny Hurkens

Zaionc paradox revisited

1 file(s) 205.52 KB Download

Proof terms for generalized classical natural deduction

1 file(s) 242.05 KB Download

On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic

1 file(s) 225.13 KB Download

Model Theory

Start TimeTitleAuthors11:30Interpreting Twisted Cubes as Partially Ordered SpacesGun Pinyo11:45B-systems and C-systems are equivalentBenedikt Ahrens, Jacopo Emmenegger, Paige North and Egbert Rijke11:55A finite-dimensional model for affine, linear quantum lambda calculi with general recursionAlejandro Díaz-Caro, Malena Ivnisky, Hernán Melgratti and Benoît Valiron12:05Semisimplicial Types in Internal Categories with FamiliesJoshua Chen and Nicolai Kraus12:15Types are internal ∞-groupoidsAntoine Allioux, Eric Finster and Matthieu Sozeau

Types are Internal ∞-groupoids

1 file(s) 167.16 KB Download

Semisimplicial Types in Internal Categories with Families

1 file(s) 293.22 KB Download

Interpreting Twisted Cubes as Partially Ordered Spaces

1 file(s) 320.26 KB Download

A finite-dimensional model for affine, linear quantum lambda calculi with general recursion

…

Logical and Semantic Principles

Start TimeTitleAuthors10:00On the logical structure of choice and bar induction principlesNuria Brede and Hugo Herbelin10:10A container model of type theoryThorsten Altenkirch and Ambrus Kaposi10:25Quantitative polynomial functorsGeorgi Nakov and Fredrik Nordvall Forsberg10:35Shape-irrelevant reflection: Terminating extensional type theoryThéo Winterhalter10:45On Model-Theoretic Strong Normalization for Truth-Table Natural DeductionAndreas Abel

Author: Henning

Opening

Social Gathering

Business Meeting

Closing Discussion

Proof Assistants Applications