Paris

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

Program

The whole schedule in pdf.

All the abstracts : book of abstracts and list of talks by authors.

Monday, May 12

9:00 Welcome and Registration
9:50 Isomorphism of Finitary Inductive Types (abstract, talk) Nicolai Kraus and Christian Sattler
10:15 Deciding unique inhabitants with sums (abstract, talk) Gabriel Scherer
10:40 Simply Typed Lambda-Calculus Modulo Type Isomorphisms (abstract, talk) Alejandro Díaz-Caro and Gilles Dowek
11:05 Inductive Construction in Nuprl Type Theory Using Bar Induction (abstract, talk) Mark Bickford and Robert Constable
11:30 Lunch
14:00 Session Types, Solos, and the Computational Contents of Sequent Calculus Proofs (abstract) Nicolas Guenot
14:25 Some Varieties of Constructive Finitenes (abstract, talk) Erik Parmann
14:50 A Calculus of Primitive Recursive Constructions (abstract, talk) Hugo Herbelin and Ludovic Patey
15:15 A Kleene realizability semantics for the Minimalist Foundation (abstract, talk) Maria Emilia Maietti, Samuele Maschio and Takako Nemoto
15:40 Coffee Break
16:10 Objects and subtyping in the lambda-Pi-calculus modulo (abstract, talk) Raphaël Cauderlier, Ali Assaf and Catherine Dubois
16:35 Toward a Theory of Contexts of Assumptions in Logical Frameworks (abstract, talk) Amy Felty, Alberto Momigliano and Brigitte Pientka
17:00 Type-Checking Linear Dependent Types (abstract, talk) Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Arias and Justin Hsu
17:25 A type system for Continuation Calculus (abstract, talk) Herman Geuvers, Wouter Geraedts, Bram Geron and Judith van Stegeren
17:50 End

Tuesday, May 13

9:00 Eliminating Higher Truncations via Constancy (abstract, talk) Paolo Capriotti and Nicolai Kraus
9:25 A decidable formulation of extensional type theory (abstract, talk) Andrew Polonsky
9:50 Covering Spaces in Homotopy Type Theory (abstract, talk) Kuen-Bang Hou (Favonia)
10:15 All derivations of groupoid laws are propositionally equal (abstract, talk) Marc Lasson
10:40 Coffee Break
11:10 A cubical set model of type theory (abstract, talk) Thierry Coquand (invited speaker)
12:10 Lunch
14:00 Pattern Matching Without K (abstract, talk) Jesper Cockx, Dominique Devriese and Frank Piessens
14:25 Exceptions in Dependent Type Theory (abstract) Jorge Luis Sacchini
14:50 Polymorphic Variants in Dependent Type Theory (abstract, talk) Dominic Mulligan and Claudio Sacerdoti Coen
15:15 Liquid Types Revisited (abstract, talk) Mário Pereira, Sandra Alves and Mário Florido
15:40 Coffee Break
16:10 Coq à la Tarski (abstract, talk) Ali Assaf
16:35 A Type Theory with Partial Equivalence Relations as Types (abstract, talk) Abhishek Anand, Mark Bickford, Robert Constable and Vincent Rahli
17:00 Towards an Internalization of the Groupoid Interpretation of Type Theory (abstract, talk) Matthieu Sozeau and Nicolas Tabareau
17:25 Proof-relevant Rewriting Strategies in Coq (abstract, talk) Matthieu Sozeau
17:50 Break
18:15 Business Meeting
19:15 End

Wednesday, May 14

9:00 Proving and computing with the Harthong-Reeb line (abstract, talk) Nicolas Magaud and Laurent Fuchs
9:25 Modular and lightweight certification of polyhedral abstract domain (abstract, talk) Alexis Fouilhe, Sylvain Boulmé and Michaël Périn
9:50 A Separation Logic for Non-determinism and Sequence Points in C Formalized in Coq (abstract, talk) Robbert Krebbers
10:15 Synthesis of Certified Programs with Effects Using Monads in Coq (abstract, talk pdf, talk animation) Sara Fabbro and Marino Miculan
10:40 Coffee Break
11:10 Formal verification of a static analyzer: abstract interpretation in type theory (abstract, talk) Xavier Leroy (invited speaker)
12:10 Lunch
14:00 A formalization of the Quipper quantum programming language (abstract, talk) Neil J. Ross
14:25 Dialectica: From Gödel to Curry-Howard (abstract, talk) Pierre-Marie Pédrot
14:50 On the complexity of negative quantification (abstract, talk) Aleksy Schubert, Pawel Urzyczyn and Konrad Zdanowski
15:15 Global semantic typing for inductive and coinductive computing (abstract) Daniel Leivant
15:40 Coffee
16:10 Free Time
19:15 Dinner at "Le vin qui danse"

Thursday, May 15

9:00 Coinitial semantics for redecoration of triangular matrices (abstract, talk) Benedikt Ahrens and Régis Spadotti
9:25 The Church-Scott representation of inductive and coinductive data in typed lambda calculus (abstract, talk) Herman Geuvers
9:50 Coinduction in Agda using Copatterns and Sized Types (abstract, talk) Andreas Abel
10:15 Coalgebraic update lenses (abstract) Danel Ahman and Tarmo Uustalu
10:40 Coffee Break
11:10 Nominal sets and dependent type theory (abstract, talk) (joint session with PCC) Andy Pitts (invited speaker)
12:10 Lunch
14:00 Higher Inductive Types as Homotopy-Initial Algebras (abstract, talk) Kristina Sojakova
14:25 Church-Rosser Theorem for sequent lambda calculi (abstract, talk) Silvia Ghilezan, Jelena Ivetic and Silvia Likavec
14:50 Type system for automated generation of reversible circuits (abstract) Benoît Valiron
15:15 Coffee & Closing  

Home

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