All of the scientific programme of the conference will happen at the House of the Blackheads (Pikk 26, in the Old Town), Olav's Hall
Monday, 18 May 2015 

8.309.00  Registration 
9.0010.00  Gilles Barthe Computeraided cryptography (slides) 
10.0010.30  João Paulo Pizani Flor, Wouter Swierstra Πware: an embedded hardware description language using dependent types (slides) 
10.3011.00  Coffee 
11.0012.30  Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, Silvia Likavec Intersection types fit well with resource control (slides) 
Noam Zeilberger Balanced polymorphism and linear lambda calculus (slides) 

Charles Grellois, PaulAndré Melliès Coloured intersection types: a semantic approach to higherorder modelchecking (slides) 

12.3014.00  Lunch 
14.0015.30  Andreas Abel (talk given by Andrea Vezzosi) The next 700 modal type assignment systems (slides) 
Henning Basold, Herman Geuvers Semantics for dependent inductive and coinductive types through dialgebras in fibrations (slides) 

Henning Basold, Herman Geuvers Dialgebrainspired syntax for dependent inductive and coinductive types (slides) 

15.3016.00  Coffee 
16.0017.30  Aleš Bizjak, Rasmus E. Møgelberg Rewrite semantics for guarded recursion with universal quantification over clocks (slides) 
Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, Lars Birkedal Guarded dependent type theory with coinductive types (slides) 

Andrea Vezzosi Total (co)programming with guarded recursion (slides) 

19.00...  Excursion to and reception at the Seaplane Harbor (Vesilennuki 6, in Kalamaja district) 
Tuesday, 19 May 2015 

9.0010.00  Andrej Bauer The troublesome reflection rule (slides) 
10.0010.30  Bas Spitters Cubical sets as a classifying topos (slides) 
10.3011.00  Coffee 
11.0012.30  Valentin Blot Typed realizability for firstorder classical analysis (slides) 
Hugo Herbelin A proof with side effects of Gödel's completeness theorem suitable for semantic normalisation (slides) 

Gert Smolka Axiomatic set theory in type theory with inductive definitions (slides) 

12.3014.00  Lunch 
14.0015.00  Danel Ahman, Gordon Plotkin Refinement types for algebraic effects (slides) 
James Chapman, Tarmo Uustalu, Niccolò Veltri Quotienting the delay monad by weak bisimilarity (slides) 

15.0015.30  Coffee 
15.3016.30  Joachim Kock Polynomial functors: a general framework for induction and substitution 
16.3017.30  Peter LeFanu Lumsdaine Higher inductive types: what we understand, what we don't 
17.4518.30  Biz meeting 
Wednesday, 20 May 2015 

9.0010.00  Peter Selinger Types for quantum computing (slides) 
10.0010.30  Robin Adams, Bart Jacobs State and effect logics for deterministic, nondeterministic, probabilistic and quantum computation (slides) 
10.3011.00  Coffee 
11.0012.30  Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus Infinite structures in type theory: problems and approaches (slides) 
James McKinna, Fredrik Nordvall Forsberg The encodedecode method, relationally (slides) 

Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik
Nordvall Forsberg Towards a theory of higher inductive types (slides) 

12.3014.00  Lunch 
14.0015.30  Étienne Miquey, Hugo Herbelin Toward dependent choice: a classical sequent calculus with dependent types (slides) 
Daniel Gustafsson, Nicolas Guenot Implementing dependent types using sequent calculi (slides) 

Zhaohui Luo A Lambek calculus with dependent types (slides) 

15.3016.00  Coffee 
16.0017.00  Cyril Cohen, Mathieu Kohli A Coq formalization of a sign determination algorithm in real algebraic geometry (slides) 
Luís CruzFilipe, Peter SchneiderKamp A formalized checker for sizeoptimal sorting networks (slides) 

19.00...  Dinner at Restaurant Platz (Roseni 7, in Rotermanni quarter) 
Thursday, 21 May 2015 

9.0010.30  Thorsten Altenkirch, Ambrus Kaposi A nominal syntax for internal parametricity (slides) 
Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo Twodimensional proofrelevant parametricity (slides) 

JeanPhilippe Bernardy, Thierry Coquand, Guilhem Moulin A presheaf model of parametric type theory (slides) 

10.3011.00  Coffee 
11.0012.30  Jorge Luis Sacchini Wellfounded sized types in the calculus of (co)inductive constructions (slides) 
Christian Sattler On relating indexed Wtypes with ordinary ones (slides) 

Benedikt Ahrens, Paolo Capriotti, Régis Spadotti Nonwellfounded trees in homotopy type theory (slides) 

12.3014.00  Lunch 
14.0015.30  Herman Geuvers A typed lambdacalculus with callbyname and callbyvalue iteration (slides) 
Ralph Matthes, Benedikt Ahrens Substitution systems revisited (slides) 

Erkki Luuk Introducing a typetheoretical approach to universal grammar 

15.3016.00  Coffee 