Accepted Contributions

Contributions

Icon

A container model of type theory 295.52 KB 24 downloads

Thorsten Altenkirch and Ambrus Kaposi ...
Icon

A drag-and-drop proof tactic 225.36 KB 14 downloads

Pablo Donato, Pierre-Yves Strub and Benjamin Werner ...
Icon

A finite-dimensional model for affine, linear quantum lambda calculi with general recursion 387.77 KB 6 downloads

Alejandro Díaz-Caro, Malena Ivnisky, Hernán Melgratti, and Benoît Valiron ...
Icon

A Formal Theory of Games of Incomplete Information 373.70 KB 5 downloads

Hélène Fargier, Érik Martin-Dorel, and Pierre Pomeret-Coquot ...
Icon

A Formalisation of Approximation Fixpoint Theory 280.01 KB 8 downloads

Bart Bogaerts and Luı́s Cruz-Filipe ...
Icon

A Gradual Intersection Typed Calculus 298.92 KB 8 downloads

Pedro Ângelo and Mário Florido ...
Icon

A Practical Implementation of Twin Types 69.24 KB 11 downloads

Víctor López Juan ...
Icon

A proof assistant for synthetic ∞-categories 247.29 KB 14 downloads

Nikolai Kudasov ...
Icon

B-systems and C-systems are equivalent 379.99 KB 12 downloads

Benedikt Ahrens, Jacopo Emmenegger, Paige North and Egbert Rijke ...
Icon

Clocked Cubical Type Theory 338.62 KB 6 downloads

Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi ...
Icon

Constructive Notions of Ordinals in Homotopy Type Theory 286.96 KB 10 downloads

Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu ...
Icon

Eliminating Infinitary Induction-induction 259.18 KB 14 downloads

Filippo Sestini and Thorsten Altenkirch ...
Icon

Equality checking for dependent type theories 280.50 KB 15 downloads

Andrej Bauer and Anja Petković ...
Icon

Family Polymorphism for Proof Extensibility 172.08 KB 15 downloads

Anastasiya Kravchuk-Kirilyuk, Yizhou Zhang and Nada Amin ...
Icon

Functorial Adapters 193.42 KB 20 downloads

Conor Mc Bride and Fredrik Nordvall Forsberg ...
Icon

Intersection Types for a Computational λ-Calculus with Global State 0.00 KB 0 downloads

Ugo de’Liguoro and Riccardo Treglia ...
Icon

M-Types and Bisimulation 239.10 KB 10 downloads

Henning Basold and Daniël Otten ...
Icon

Modalities and Parametric Adjoints 220.19 KB 7 downloads

Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto, Lars Birkedal ...
Icon

Modelling Smart Contracts of Bitcoin in Agda 309.30 KB 11 downloads

Anton Setzer and Bogdan Gabriel Lazar ...