The workshop sessions will take place in the Fraternity Hall of Mustpeade Maja (House of the
Brotherhood of Blackheads), Pikk 26, in the Old Town.
| Wednesday, 14 April | ||
| 08:30-09:00 | Registration | |
| 09:00-10:00 | Philip Wadler
Call-by-value is dual to call-by-name |
|
| 10:00-10:30 | Helmut Schwichtenberg
Computational content of the intermediate value theorem |
|
| José Espírito Santo, Luís Pinto
The multiary version of the lambda-calculus with generalized application |
||
| 10:30-11:00 | Coffee | |
| 11:00-12:30 | Sandra Alves, Mário Florido
Linearization by program transformation |
|
| Michael Abbott, Thorsten Altenkirch, Neil Ghani
Representing nested inductive types using W-types |
||
| David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu
Extracting a data flow analyser in constructive logic |
||
| 12:30-14:00 | Lunch in the Cellar Hall, House of the Brotherhood of Blackheads | |
| 14:00-15:00 | Antoine Galland, Mathieu Baudet
A resource-control model based on deadlock avoidance |
|
| David von Oheimb, Volkmar Lotz
Formal security analysis at Siemens Corporate Technology |
||
| Margus Veanes
The future of black-box testing at Microsoft |
||
| 15:00-15:45 | Industrial panel session | |
| 15:45-16:15 | Coffee | |
| 16:15-18:00 | Industrial panel session | |
| 19:30- | Reception in the White Hall, House of the Brotherhood of Blackheads | |
| Thursday, 15 April | ||
| 09:00-10:00 | Sriram Rajamani
SLAM: software model checking from theory to practice |
|
| 10:00-10:30 | James Leifer, Michael Norrish, Peter Sewell, Keith Wansbrough
Acute and TCP: specifying and developing abstractions for global computation |
|
| Andrei Serjantov
On the anonymity of message-based anonymity systems |
||
| 10:30-11:00 | Coffee | |
| 11:00-11:30 | Kamal Lodaya, Uday S. Reddy
Grainless concurrency semantics for monitors |
|
| Olivier Bournez, Felipe Cucker, Paulin Jacobe de Naurois, Jean-Yves Marion
Tayloring recursion to characterize non-deterministic complexity classes over arbitrary structures |
||
| 11:30-12:30 | Olivier Bournez, Emmanuel Hainry
An analog characterization of computable functions over the real numbers |
|
| Philippa Gardner, Sergio Maffeis
Modelling dynamic web data |
||
| 12:30-14:00 | Lunch | |
| 14:00-15:45 | Anuj Dawar, Philippa Gardner, Giorgio Ghelli
Games for ambient logic |
|
| Luís Caires, Antonio Ravara
Spatial types for processes |
||
| Matthew Parkinson
When separation logic meets Java |
||
| Didier Galmiche, J. Gobillot, Daniel Méry
Proofs and countermodels in BI's pointer logic |
||
| Nicolas Biri, Didier Galmiche
A separation logic for resource distribution |
||
| Robert Atkey
A categorical semantics for resource separation |
||
| Paul Taylor
Review of abstract Stone duality |
||
| 15:45-16:15 | Coffee | |
| 16:15-18:00 | Jaan Penjam, Varmo Vene
Wreath products of generalized automata |
|
| Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
Constructing polymorphic programs with quotient types |
||
| Marcin Benke, Makoto Takeyama
Generic proofs and programs for coinductive types in Martin- Löf's type theory |
||
| Jeremy Gibbons
Patterns in datatype-generic programming |
||
| Andreas Abel
Sized higher-order datatypes |
||
| Martin Hofmann
Certification of parameter size with dependent ML |
||
| David Wahlstedt
Type theory with first-order data types and size-change termination |
||
| 18:00-19:00 | Site/theme leaders meeting | |
| 19:30- | Conference dinner at Restaurant Maikrahv, Raekoja plats 8 | |
| Friday, 16 April | ||
| 09:00-10:00 | Jim Laird
Extensional semantics of program behaviors |
|
| 10:00-10:30 | Tobias Löw
A universal model for an infinitary version of sequential PCF |
|
| Paul Levy
Infinite trace semantics |
||
| 10:30-11:00 | Coffee | |
| 11:00-12:30 | Guillaume Bonfante, Jean-Yves Marion, Jean-Yves Moyen
On complexity analysis by quasi-interpretation |
|
| Mark R. Shinwell, Andrew M. Pitts
On a monadic semantics for freshness |
||
| Mads Sig Ager, Olivier Danvy, Jan Midtgaard
A functional correspondence between monadic evaluators and abstract machines for languages with computational effects |
||
| 12:30-14:00 | Lunch | |
| 14:00-15:45 | Davide Ancona, Eugenio Moggi
A calculus for symbolic names management |
|
| Graham Hutton, Joel Wright
Compiling exceptions correctly |
||
| Nils Anders Danielsson, Patrik Jansson
Chasing bottoms - a case study in program verification in the presence of partial and infinite values |
||
| Johan Erikson, Björn Lisper
A formal semantics for PLEX |
||
| Tom Hirschowitz, Xavier Leroy, Joe Wells
Extended recursive definitions in call-by-value languages, with applications to mixin modules and recursive modules |
||
| Nadji Gauthier, Francois Pottier
Efficient unification of recursive second-order types |
||
| Jeremy Singer
Sparse bidirectional data flow analysis as a basis for type inference | ||
| 15:45-16:15 | Coffee | |
| 16:15-17:15 | Jeremy Gibbons
Streaming algorithms |
|
| Alcino Cunha, Jorge Sousa Pinto
Making the point-free calculus less point-less |
||
| John Longley, Randy Pollack
Reasoning about CBV functional programs in Isabelle/HOL |
||
| Fredrik Lindblad, Marcin Benke
An experiment in automated theorem proving in type theory |
||
| 17:15-18:00 | Business meeting | |