Book of Abstracts
TYPES 2021 - Book of Abstracts
1 file(s) 11 MB
List of Contributions
| Title | Authors | Session |
|---|---|---|
| A Gradual Intersection Typed Calculus | Pedro Ângelo and Mário Florido | Computation and Intersection Types |
| Intersection Types for a Computational Lambda-Calculus with Global State | Ugo De’Liguoro and Riccardo Treglia | Computation and Intersection Types |
| The syntactic tale of the oracle and the trees | Martin Baillon and Pierre-Marie Pédrot | Computation and Intersection Types |
| Novel rules of β-conversion in partial type theory | Jiří Raclavský and Petr Kuchyňka | Computation and Intersection Types |
| Quotient inductive-inductive types in the setoid model | Ambrus Kaposi and Zongpu Xie | Inductive Types |
| Eliminating Infinitary Induction-induction | Filippo Sestini and Thorsten Altenkirch | Inductive Types |
| Simulating large eliminations in Cedille | Christopher Jenkins, Andrew Marmaduke and Aaron Stump | Inductive Types |
| A container model of type theory | Thorsten Altenkirch and Ambrus Kaposi | Logical and Semantic Principles |
| Quantitative polynomial functors | Georgi Nakov and Fredrik Nordvall Forsberg | Logical and Semantic Principles |
| Shape-irrelevant reflection: Terminating extensional type theory | Théo Winterhalter | Logical and Semantic Principles |
| On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction | Andreas Abel | Logical and Semantic Principles |
| On the logical structure of choice and bar induction principles | Nuria Brede and Hugo Herbelin | Logical and Semantic Principles |
| Modalities and Parametric Adjoints | Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto and Lars Birkedal | Modal Type Theory |
| Normalization for multimodal type theory | Daniel Gratzer | Modal Type Theory |
| Clocked Cubical Type Theory | Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg and Andrea Vezzosi | Modal Type Theory |
| Semantic Analysis of Normalization by Evaluation for Fitch-Style Modal Lambda Calculi | Nachiappan Valliappan, Fabian Ruch and Carlos Tomé Cortiñas | Modal Type Theory |
| Interpreting Twisted Cubes as Partially Ordered Spaces | Gun Pinyo | Model Theory |
| B-systems and C-systems are equivalent | Benedikt Ahrens, Jacopo Emmenegger, Paige North and Egbert Rijke | Model Theory |
| A finite-dimensional model for affine, linear quantum lambda calculi with general recursion | Alejandro Díaz-Caro, Malena Ivnisky, Hernán Melgratti and Benoît Valiron | Model Theory |
| Semisimplicial Types in Internal Categories with Families | Joshua Chen and Nicolai Kraus | Model Theory |
| Types are internal infinity-groupoids | Antoine Allioux, Eric Finster and Matthieu Sozeau | Model Theory |
| Syntax for two-level type theory | Roberta Bonacina and Benedikt Ahrens | New Type Theories |
| Using Two-Level Type Theory for Staged Compilation | András Kovács | New Type Theories |
| Native Type Theory | Christian Williams and Michael Stay | New Type Theories |
| Functorial Adapters | Conor Mcbride and Fredrik Nordvall Forsberg | New Type Theories |
| Type theories without contexts | Andrej Bauer and Philipp G. Haselwarter | New Type Theories |
| Equality checking for dependent type theories | Andrej Bauer and Anja Petković | Proof Assistants Foundations |
| Family Polymorphism for Proof Extensibility | Anastasiya Kravchuk-Kirilyuk, Yizhou Zhang and Nada Amin | Proof Assistants Foundations |
| A Drag-and-Drop Proof Tactic | Benjamin Werner, Pablo Donato and Pierre-Yves Strub | Proof Assistants Foundations |
| A proof assistant for synthetic ∞-categories | Nikolai Kudasov | Proof Assistants Foundations |
| A Practical Implementation of Twin Types | Víctor López Juan | Proof Assistants Foundations |
| Modelling Smart Contracts of Bitcoin in Agda | Anton Setzer and Bogdan Gabriel Lazar | Proof Assistants Applications |
| The Agda Universal Algebra Library and Birkhoff’s Theorem in Dependent Type Theory | William DeMeo | Proof Assistants Applications |
| A Formal Theory of Games of Incomplete Information | Helene Fargier, Érik Martin-Dorel and Pierre Pomeret-Coquot | Proof Assistants Applications |
| SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq | Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hritcu, Kenji Maillard and Bas Spitters | Proof Assistants Applications |
| Towards Automation for Iris | Ike Mulder and Robbert Krebbers | Proof Assistants Applications |
| On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic | Asta Halkjær From and Jørgen Villadsen | Proof Theory |
| Zaionc paradox revisited | Pierre Lescanne | Proof Theory |
| Proof terms for generalized classical natural deduction | Herman Geuvers and Tonny Hurkens | Proof Theory |
| Size-Based Termination for Non-Positive Types | Yuta Takahashi | Recursion |
| Constructive Notions of Ordinals in Homotopy Type Theory | Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu | Recursion |
| Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor | Niccolò Veltri | Recursion |
| A Formalisation of Approximation Fixpoint Theory | Bart Bogaerts and Luís Cruz-Filipe | Recursion |
| M-types and Bisimulation | Daniël Otten and Henning Basold | Recursion |