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

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

…

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

…

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

Shape-irrelevant reflection: Terminating extensional type theory

1 file(s) 62.39 KB Download

Quantitative polynomial functors

1 file(s) 253.57 KB Download

On the logical structure of choice and bar induction principles

1 file(s) 295.47 KB Download

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction

1 file(s) 202.43 KB Download…

Start TimeTitleAuthors11:30A Gradual Intersection Typed CalculusPedro Ângelo and Mário Florido11:45Intersection Types for a Computational Lambda-Calculus with Global StateUgo De’Liguoro and Riccardo Treglia11:55The syntactic tale of the oracle and the treesMartin Baillon and Pierre-Marie Pédrot12:10Novel rules of β-conversion in partial type theoryJiří Raclavský and Petr Kuchyňka

The syntactic tale of the oracle and the trees A model of continuity in a dependent setting

1 file(s) 334.49 KB Download

Novel rules of β-conversion in partial type theory

1 file(s) 350.09 KB Download

A Gradual Intersection Typed Calculus

1 file(s) 298.92 KB Download

Intersection Types for a Computational λ-Calculus with Global State

1 file(s) Read more Computation and Intersection Types →