Programme

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.30-9.00 Registration
9.00-10.00 Gilles Barthe
Computer-aided cryptography
10.00-10.30 João Paulo Pizani Flor, Wouter Swierstra
Π-ware: an embedded hardware description language using dependent types
10.30-11.00 Coffee
11.00-12.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, Paul-André Melliès
Coloured intersection types: a semantic approach to higher-order model-checking
12.30-14.00 Lunch
14.00-15.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
Dialgebra-inspired syntax for dependent inductive and coinductive types
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
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.00-10.00 Andrej Bauer
The troublesome reflection rule
10.00-10.30 Bas Spitters
Cubical sets as a classifying topos
10.30-11.00 Coffee
11.00-12.30 Valentin Blot
Typed realizability for first-order 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.30-14.00 Lunch
14.00-15.00 Danel Ahman, Gordon Plotkin
Refinement types for algebraic effects
James Chapman, Tarmo Uustalu, Niccolò Veltri
Quotienting the delay monad by weak bisimilarity
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
10.00-10.30 Robin Adams, Bart Jacobs
State and effect logics for deterministic, non-deterministic, probabilistic and quantum computation
10.30-11.00 Coffee
11.00-12.30 Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
Infinite structures in type theory: problems and approaches
James McKinna, Fredrik Nordvall Forsberg
The encode-decode method, relationally
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik Nordvall Forsberg
Towards a theory of higher inductive types
12.30-14.00 Lunch
14.00-15.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.30-16.00 Coffee
16.00-17.00 Cyril Cohen, Mathieu Kohli
A Coq formalization of a sign determination algorithm in real algebraic geometry
Luís Cruz-Filipe, Peter Schneider-Kamp
A formalized checker for size-optimal sorting networks
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
Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo
Two-dimensional proof-relevant parametricity
Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
A presheaf model of parametric type theory
10.30-11.00 Coffee
11.00-12.30 Jorge Luis Sacchini
Well-founded sized types in the calculus of (co)inductive constructions
Christian Sattler
On relating indexed W-types with ordinary ones
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
Non-wellfounded trees in homotopy type theory
12.30-14.00 Lunch
14.00-15.30 Herman Geuvers
A typed lambda-calculus with call-by-name and call-by-value iteration
Ralph Matthes, Benedikt Ahrens
Substitution systems revisited
Erkki Luuk
Introducing a type-theoretical approach to universal grammar
15.30-16.00 Coffee

Tarmo Uustalu
Last update 15 May 2015