All of the scientific programme of the conference will happen at the House of 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 
10.0010.30  João Paulo Pizani Flor, Wouter Swierstra Πware: an embedded hardware description language using dependent types 
10.3011.00  Coffee 
11.0012.30  Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, Silvia Likavec Intersection types fit well with resource control 
Noam Zeilberger Balanced polymorphism and linear lambda calculus 

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

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

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

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

Andrea Vezzosi Total (co)programming with guarded recursion 

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 
10.0010.30  Bas Spitters Cubical sets as a classifying topos 
10.3011.00  Coffee 
11.0012.30  Valentin Blot Typed realizability for firstorder classical analysis 
Hugo Herbelin A proof with side effects of Gödel's completeness theorem suitable for semantic normalisation 

Gert Smolka Axiomatic set theory in type theory with inductive definitions 

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

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 
10.0010.30  Robin Adams, Bart Jacobs State and effect logics for deterministic, nondeterministic, probabilistic and quantum computation 
10.3011.00  Coffee 
11.0012.30  Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus Infinite structures in type theory: problems and approaches 
James McKinna, Fredrik Nordvall Forsberg The encodedecode method, relationally 

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

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

Zhaohui Luo A Lambek calculus with dependent types 

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

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 
Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo Twodimensional proofrelevant parametricity 

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

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

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

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

Erkki Luuk Introducing a typetheoretical approach to universal grammar 

15.3016.00  Coffee 