Final Program †
NEWS: The program has CHANGED because many flights from Europe were canceled.
NEWS: Fritz Henglein and Oliver Danvy gave new invited talks.
April 19 (Monday) †
11:30-13:20 Registration and lunch †
13:20-14:20 Invited talk †
- Solving Constraint Satisfaction Problems with SAT Technology
- Naoyuki Tamura
14:40-16:10 Evaluation and normalization †
- Internal Normalization, Compilation and Decompilation for System F
- Stefano Berardi, Makoto Tatsuta
- Normalization by Evaluation for the beta-eta Calculus of Constructions
- Andreas Abel
- Defunctionalized Interpreters for Call-by-Need Evaluation
- Olivier Danvy, Kevin Millikin, Johan Munk, Ian Zerny
16:30-18:00 Types and program transformation †
- A Church-Style Intermediate Language for MLF
- Didier Remy, Boris Yakobowski
- Tagfree Combinators for Binding-Time Polymorphic Program Generation
- Peter Thiemann, Martin Sulzmann
- Automatic Parallelization of Recursive Functions using Quantifier Elimination
- Akimasa Morihata, Kiminori Matsuzaki
April 20 (Tuesday) †
09:00-10:00 Invited talk †
- Generic Top-down Discrimination: Sorting and partitioning without compare
- Fritz Henglein
10:20-11:50 Term rewriting †
- Complexity Analysis by Graph Rewriting
- Martin Avanzini, Georg Moser
- Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus
- Jeroen Ketema, Jakob Grue Simonsen
- Proving Injectivity of Functions via Program Inversion in Term Rewriting
- Naoki Nishida, Masahiko Sakai
11:50- Lunch (in the bus) and excursion to Hiraizumi (bus leaves conference venue at 12:30) †
April 21 (Wednesday) †
09:00-10.00 Invited talk †
- Using Static Analysis to Detect Type Errors and Race Conditions in Erlang Programs
- Konstantinos Sagonas
10:20-11:50 †
- Delimited Control in OCaml, Abstractly and Concretely. System Description
- Oleg Kiselyov
- A Functional Framework for Result Checking
- Gilles Barthe, Pablo Buiras, César Kunz
- ΠΣ: Dependent Types without the Sugar
- Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury (Speaker: Andreas Abel)
11:50- Lunch and Video Talks †
- A Skeleton for Distributed Work Pools in Eden
- Mischa Dieterle, Jost Berthold, Rita Loogen
- Code Generation via Higher-Order Rewrite Systems
- Florian Haftmann, Tobias Nipkow
- A Pearl on SAT Solving in Prolog
- Jacob Howe, Andy King
- Haskell Type Constraints Unleashed
- Dominic Orchard, Tom Schrijvers
- Automatically Generating Counterexamples to Naive Free Theorems
- Daniel Seidel, Janis Voigtländer
14:00-15:30 †
- A Complete Axiomatization of Strict Equality
- Javier Álvez, Francisco Javier López-Fraguas
- An Integrated Distance for Atoms
- Vicent Estruch, César Ferri, José Hernández-Orallo, M.José Ramírez-Quintana
- Applying Constraint Logic Programming to SQL Test Case Generation
- Yolanda García-Ruiz, Rafael Caballero, Fernando Sáenz-Pérez
16:00-17:30 †
- Standardization and Böhm trees for Lambda-mu calculus
- Alexis Saurin
- CPS for ever (invited talk)
- Olivier Danvy