Accepted Papers

TYPES 2018 Accepted Papers

Reinhard Kahle and Anton Setzer. Beyond the limits of the Curry-Howard isomorphism
Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation
Taichi Uemura. Cubical Assemblies and Independence of the Propositional Resizing Axiom
Benedikt Ahrens and Marco Maggesi. A modular formalization of bicategories in type theory
András Kovács. Closure Conversion for Dependent Type Theory, With Type-Passing Polymorphism
Ambroise Lafont, Tom Hirschowitz and Nicolas Tabareau. Types are weak omega-groupoids, in Coq
Filippo Sestini. Towards Normalization for the Minimal Type Theory
Silvia Ghilezan, Jelena Ivetic, Simona Kasterovic, Zoran Ognjanovic and Nenad Savic. Towards probabilistic reasoning about typed lambda terms
Anton Setzer. Simulating Codata Types using Coalgebras
Valentin Blot and James Laird. Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
Davide Ancona, Giuseppe Castagna, Tommaso Petrucciani and Elena Zucca. Semantic subtyping for non-strict languages
Beniamino Accattoli, Andrea Condoluci and Claudio Sacerdoti Coen. Sharing Equality is Linear
Jesper Cockx, Gaëtan Gilbert and Nicolas Tabareau. Vectors are records, too
Bassel Mannaa and Rasmus Møgelberg. The clocks they are adjunctions: Denotational semantics for Clocked Type Theory
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew Pitts and Bas Spitters. Dependent Right Adjoint Types
Pierre Vial. Typing every λ-term with infinitary non-idempotent types
Paola Giannini, Tim Richter, Marco Servetto and Elena Zucca. Towards a mechanized soundness proof for sharing effects
Thorsten Altenkirch, Ambrus Kaposi, András Kovács and Jakob von Raumer. Reducing Inductive-Inductive Types to Indexed Inductive Types
Dominique Larchey-Wendling and Jean-François Monin. Simulating Induction-Recursion for Partial Algorithms
Cesare Gallozzi. A Comparative Analysis of Type-Theoretic Interpretations of Constructive Set Theories
Gun Pinyo and Thorsten Altenkirch. Integers as a Higher Inductive Type
Théo Winterhalter, Matthieu Sozeau and Nicolas Tabareau. Using reflection to eliminate reflection
Steven Schäfer and Kathrin Stark. Embedding Higher-Order Abstract Syntax in Type Theory
Henning Basold. The Later Modality in Fibrations
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani and Jeremy Siek. Polymorphic Gradual Typing: A Set-Theoretic Perspective
Mirko Spasić and Milena Vujošević Janičić. First steps towards proving functional equivalence of embedded SQL
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus and Fredrik Nordvall Forsberg. Specifying Quotient Inductive-Inductive Types
Sergei Soloviev and Ian Malakhovsky. Automorphisms of Types for Security and Trust
Andreas Abel. Resourceful dependent types
Herman Geuvers, Iris van der Giessen and Tonny Hurkens. Cut-elimination for general constructive proposition logic
Étienne Miquey. How delimited continuations can be used to define dependently typed CPS
Nicolai Kraus. On the Role of Semisimplicial Types
Paige North. A type theory for directed homotopy theory
Thorsten Altenkirch, Péter Diviánszky, Ambrus Kaposi and András Kovács. Constructing inductive-inductive types using a domain-specific type theory
Ugo De Liguoro and Luca Padovani. Mailbox Types for Unordered Interactions
Zhaohui Luo. Formal Semantics in Modern Type Theories
Vasco T. Vasconcelos, Antónia Lopes and Francisco Martins. HeadREST: A Specification Language for RESTful APIs
Sophie Bernard. A Constructive Morphism between Algebraic Fields and (Real-)Closed Fields
Luís Afonso Carvalho, João Costa Seco and Jácome Cunha. Typing the Evolution of Variational Software
Bogdan Aman and Gabriel Ciobanu. Session Types for Timed Migration
Tõnn Talvik and Tarmo Uustalu. Experimenting with graded monads: certified grading-based program transformations
Luigi Liquori and Claude Stolze. Characterization of eight intersection type systems `a la Church
Hugo Herbelin. Syntactic investigations into cubical type theory
Niels van der Weide, Dan Frumin and Herman Geuvers. 1-Types versus Groupoids