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