Invited Speakers   

Simona Ronchi Della Rocca. Intersection Types for denotational semantics

Dale Miller. Mechanized metatheory revisited 

Simon Gay. Session Types: Achievements and Challenges

 

Book of abstracts - single file

Silvia Ghilezan and Jelena Ivetic, editors

 

TYPES 2016 Accepted Papers

Ohad Kammar, Sean Moss and Matija Pretnar. No value restriction is needed for algebraic effects and handlers
Randy Pollack and Masahiko Sato. β reduction without rule ξ
Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types
Jesper Cockx and Andreas Abel. Sprinkles of extensionality for your vanilla type theory
Robin Adams, Marc Bezem and Thierry Coquand. A Strongly Normalizing Computation Rule for the Univalence Axiom in Higher-Order Propositional Logic
Jan Bessai, Andrej Dudenhefner, Boris Duedder and Jakob Rehof. Extracting a formally verified Subtyping Algorithm for Intersection Types from Ideals and Filters
Jan Bessai, Andrej Dudenhefner, Boris Duedder and Jakob Rehof. Rank 3 Inhabitation of Intersection Types Revisited
Sergei Soloviev. Automorphisms of Types, Cayley Graphs and Representation of Finite Groups
Zhaohui Luo and Yu Zhang. A Linear Dependent Type Theory
Silvia Ghilezan, Jelena Ivetic, Zoran Ognjanovic and Nenad Savic. Towards probabilistic reasoning about lambda terms with intersection types
Pierre-Louis Curien and Jovana Obradović. A formal language for cyclic operads
Auke Booij. Parametricity and excluded middle
Pierre-Marie Pédrot, Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau and Gabriel Lewertowski. The Definitional Side of the Forcing
Andreas Abel, Thierry Coquand and Bassel Mannaa. On the Decidability of Conversion in Type Theory
Pierre-Marie Pédrot and Andrej Bauer. The Dialectica Translation of Type Theory
Andreas Abel and Théo Winterhalter. An Extension of Martin-Löf Type Theory with Sized Types
Andrew Polonsky and Giulio Manzonetto. On Unification of Lambda Terms
Adam Sandberg Eriksson and Patrik Jansson. FLABloM: Functional linear algebra with block matrices
Ralph Matthes. A Structural Approach to the Stretching Lemma of Simply-Typed Lambda-Calculus
Thorsten Altenkirch and Nils Anders Danielsson. Partiality, Revisited
Andrej Bauer. On self-interpreters for Gödel's System T
Gilles Dowek. Expressing theories in the lambda-Pi-calculus modulo theory and in the Dedukti system
Valentin Blot. Hybrid realizability for intuitionistic and classical choice
Anton Setzer. The Use of the Coinduction Hypothesis in Coinductive Proofs
Nicolai Kraus. Non-Recursive Truncations
Łukasz Czajka and Cezary Kaliszyk. Components of a Hammer for Type Theory: Coq Goal Translation and Reconstruction
Colin Riba. A Dialectica-Like Approach to Tree Automata
Marco Carbone, Fabrizio Montesi and Carsten Schuermann. Towards a Logic of Multi-Party Sessions
Bogdan Aman and Gabriel Ciobanu. Type Inference for Ratio Control Multiset-Based Systems
Aleksy Schubert and Pawel Urzyczyn. Answer Set Programming in Intuitionistic Logic
Jakob von Raumer. My Experience with the Lean Theorem Prover
Jacek Chrząszcz and Aleksy Schubert. Towards Readable Program Correctness Proofs in Coq
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters and Andrea Vezzosi. Guarded cubical type theory
Bashar Alkhawaldeh and Anton Setzer. Representing the Process Algebra CSP in Type Theory
Thorsten Altenkirch, Paolo Capriotti and Nicolai Kraus. Higher Categories in Homotopy Type Theory
Paola Giannini, Elena Zucca and Marco Servetto. An imperative calculus for unique access and immutability
Étienne Miquey and Hugo Herbelin. A computational reduction of dependent choice in classical logic to system F
James Chapman and Andreas Abel. Normalization by Evaluation in the Delay Monad
Marina Lenisa, Furio Honsell, Ivan Scagnetto and Luigi Liquori. On the Set Theory of Fitch-Prawitz
Andrej Bauer, Gaëtan Gilbert, Philipp Haselwarter, Matija Pretnar and Christopher A. Stone. Design and Implementation of the Andromeda proof assistant
Adam Naumowicz and Josef Urban. A Guide to the Mizar Soft Type System
José Espírito Santo, Maria João Frade and Luís Pinto. Computing with intuitionistic sequent proof terms: progress report
Neil Ghani, Fredrik Nordvall Forsberg and Alex Simpson. A Type Theory for Comprehensive Parametric Polymorphism
Ulrik Buchholtz and Egbert Rijke. The quaternionic Hopf fibration in homotopy type theory
Henning Basold and Herman Geuvers. Type Theory based on Dependent Inductive and Coinductive Types
Herman Geuvers and Tonny Hurkens. If-then-else and other constructive and classical connectives