TYPES 2014 in Paris (May 12-15, 2014)

Talk Abstracts and Slides

The complete Book of Abstracts (1.7 Mb).

All the talks, listed in chronological order.

Invited Speakers

Thierry Coquand,
University of Gothenburg, Sweden
A cubical set model of type theory (abstract, talk)
Xavier Leroy,
Inria Paris - Rocquencourt, France
Formal verification of a static analyzer: abstract interpretation in type theory (abstract, talk)
(Joint work with David Pichardie, Sandrine Blazy, Jacques-Henri Jourdan, Vincent Laporte)
Andy Pitts,
University of Cambridge, UK
Nominal sets and dependent type theory (abstract, talk)

Contributed Talks

Andreas Abel Coinduction in Agda using Copatterns and Sized Types (abstract, talk)
Danel Ahman and Tarmo Uustalu Coalgebraic update lenses (abstract)
Benedikt Ahrens and Régis Spadotti Coinitial semantics for redecoration of triangular matrices (abstract, talk)
Abhishek Anand, Mark Bickford, Robert Constable and Vincent Rahli A Type Theory with Partial Equivalence Relations as Types (abstract, talk)
Ali Assaf Coq à la Tarski (abstract, talk)
Mark Bickford and Robert Constable Inductive Construction in Nuprl Type Theory Using Bar Induction (abstract, talk)
Paolo Capriotti and Nicolai Kraus Eliminating Higher Truncations via Constancy (abstract, talk)
Raphaël Cauderlier, Ali Assaf and Catherine Dubois Objects and subtyping in the lambda-Pi-calculus modulo (abstract, talk)
Jesper Cockx, Dominique Devriese and Frank Piessens Pattern matching without K (abstract, talk)
Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias and Justin Hsu Type-Checking Linear Dependent Types (abstract, talk)
Alejandro Díaz-Caro and Gilles Dowek Simply Typed Lambda-Calculus Modulo Type Isomorphisms (abstract, talk)
Sara Fabbro and Marino Miculan Synthesis of certified programs with effects using monads in Coq (abstract, talk pdf, talk animation)
Amy Felty, Alberto Momigliano and Brigitte Pientka Toward a Theory of Contexts of Assumptions in Logical Frameworks (abstract, talk)
Alexis Fouilhe, Sylvain Boulmé and Michaël Périn Modular and lightweight certification of polyhedral abstract domain (abstract, talk)
Herman Geuvers The Church-Scott representation of inductive and coinductive data in typed lambda calculus (abstract, talk)
Herman Geuvers, Wouter Geraedts, Bram Geron and Judith van Stegeren A type system for Continuation Calculus (abstract, talk)
Silvia Ghilezan, Jelena Ivetic and Silvia Likavec Church-Rosser Theorem for sequent lambda calculi (abstract, talk)
Nicolas Guenot Session Types, Solos, and the Computational Contents of Sequent Calculus Proofs (abstract)
Kuen-Bang Hou (Favonia) Covering Spaces in Homotopy Type Theory (abstract, talk)
Nicolai Kraus and Christian Sattler Isomorphism of Finitary Inductive Types (abstract, talk)
Robbert Krebbers A Separation Logic for Non-determinism and Sequence Points in C Formalized in Coq (abstract, talk)
Marc Lasson All derivations of coherence laws are propositionally equal (abstract, talk)
Daniel Leivant Global semantic typing for inductive and coinductive computing (abstract)
Nicolas Magaud and Laurent Fuchs Proving and computing with the Harthong-Reeb line (abstract, talk)
Maria Emilia Maietti and Samuele Maschio A Kleene realizability semantics for the Minimalist Foundation (abstract, talk)
Dominic Mulligan and Claudio Sacerdoti Coen Polymorphic variants in dependent type theory (abstract, talk)
Erik Parmann Some Varieties of Constructive Finitenes (abstract, talk)
Ludovic Patey and Hugo Herbelin A Calculus of Primitive Recursive Constructions (abstract, talk)
Mário Pereira, Sandra Alves and Mário Florido Liquid Types Revisited (abstract, talk)
Andrew Polonsky A decidable formulation of extensional type theory (abstract, talk)
Pierre-Marie Pédrot Dialectica: From Gödel to Curry-Howard (abstract, talk)
Neil J. Ross A formalization of the Quipper quantum programming language (abstract, talk)
Jorge Luis Sacchini Exceptions in Dependent Type Theory (abstract)
Gabriel Scherer Deciding unique inhabitants with sums (abstract, talk)
Aleksy Schubert, Pawel Urzyczyn and Konrad Zdanowski On the complexity of negative quantification (abstract, talk)
Kristina Sojakova Higher Inductive Types as Homotopy-Initial Algebras (abstract, talk)
Matthieu Sozeau Proof-relevant rewriting strategies in Coq (abstract, talk)
Matthieu Sozeau and Nicolas Tabareau Towards an Internalization of the Groupoid Interpretation of Type Theory (abstract, talk)
Benoît Valiron Type system for automated generation of reversible circuits (abstract, talk)


Copyright: Louvre image © Benh LIEU SONG (CC wikipedia), Annotated map © the OpenStreetMap contributors.