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.30-9.00 Registration
9.00-10.00 Gilles Barthe
Computer-aided cryptography (slides)
10.00-10.30 João Paulo Pizani Flor, Wouter Swierstra
Π-ware: an embedded hardware description language using dependent types (slides)
10.30-11.00 Coffee
11.00-12.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, Paul-André Melliès
Coloured intersection types: a semantic approach to higher-order model-checking (slides)
12.30-14.00 Lunch
14.00-15.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
Dialgebra-inspired syntax for dependent inductive and coinductive types (slides)
15.30-16.00 Coffee
16.00-17.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.00-10.00 Andrej Bauer
The troublesome reflection rule (slides)
10.00-10.30 Bas Spitters
Cubical sets as a classifying topos (slides)
10.30-11.00 Coffee
11.00-12.30 Valentin Blot
Typed realizability for first-order 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.30-14.00 Lunch
14.00-15.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.00-15.30 Coffee
15.30-16.30 Joachim Kock
Polynomial functors: a general framework for induction and substitution
16.30-17.30 Peter LeFanu Lumsdaine
Higher inductive types: what we understand, what we don't
17.45-18.30 Biz meeting

Wednesday, 20 May 2015

9.00-10.00 Peter Selinger
Types for quantum computing (slides)
10.00-10.30 Robin Adams, Bart Jacobs
State and effect logics for deterministic, non-deterministic, probabilistic and quantum computation (slides)
10.30-11.00 Coffee
11.00-12.30 Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
Infinite structures in type theory: problems and approaches (slides)
James McKinna, Fredrik Nordvall Forsberg
The encode-decode method, relationally (slides)
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik Nordvall Forsberg
Towards a theory of higher inductive types (slides)
12.30-14.00 Lunch
14.00-15.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.30-16.00 Coffee
16.00-17.00 Cyril Cohen, Mathieu Kohli
A Coq formalization of a sign determination algorithm in real algebraic geometry (slides)
Luís Cruz-Filipe, Peter Schneider-Kamp
A formalized checker for size-optimal sorting networks (slides)
19.00-... Dinner at Restaurant Platz (Roseni 7, in Rotermanni quarter)

Thursday, 21 May 2015

9.00-10.30 Thorsten Altenkirch, Ambrus Kaposi
A nominal syntax for internal parametricity (slides)
Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo
Two-dimensional proof-relevant parametricity (slides)
Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
A presheaf model of parametric type theory (slides)
10.30-11.00 Coffee
11.00-12.30 Jorge Luis Sacchini
Well-founded sized types in the calculus of (co)inductive constructions (slides)
Christian Sattler
On relating indexed W-types with ordinary ones (slides)
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
Non-wellfounded trees in homotopy type theory (slides)
12.30-14.00 Lunch
14.00-15.30 Herman Geuvers
A typed lambda-calculus with call-by-name and call-by-value iteration (slides)
Ralph Matthes, Benedikt Ahrens
Substitution systems revisited (slides)
Erkki Luuk
Introducing a type-theoretical approach to universal grammar
15.30-16.00 Coffee

Tarmo Uustalu
Last update 21 June 2015