2nd APPSEM II Workshop, APPSEM'04

Tallinn, Estonia, 14-16 April 2004


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 Lw
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

Organizers, appsem04(at)cs.ioc ee
Last update 8 April 2004