Session 1. Nonmonotonic reasoning | ||
11:00 - 12.00 | Georg Gottlob | Theory Curbing and its
Complexity
(invited talk) |
Lunch | ||
Session 2. Descriptive complexity | ||
14.30 - 15.30 | Bruno Courcelle | Graph operations and
monadic
second-order logic
(invited talk) |
15.30 - 16.00 | J.-Y. Marion,
J.-Y. Moyen |
Efficient first order
functional
program interpreter
with time bound certifications |
Coffee break | ||
Session 3. Specification and automatic proof-assistants | ||
16.30 - 17.00 | Wolfgang Grieskamp,
Markus Lepper |
Encoding Temporal Logics
in
Executable Z:
A Case Study for the ZETA System |
17.00 - 17.30 | Slawomir Lasota | Behavioural constructor
implementation
for
regular algebras |
17.30 - 18.00 | Thomas Hallgren,
Aarne Ranta |
An Extensible Proof Text Editor |
18.00 - 18.30 | David Delahaye | A Tactic Language for the System Coq |
Welcoming dinner (19:00) |
Session 4. Theorem proving | ||
8.30 - 9.00 | Miyuki Koshimura,
Ryuzo Hasegawa |
Proof Simplification for
Model
Generation and
Its Applications |
9.00 - 9.30 | Christian G. Fermüuller,
Georg Moser |
Have SPASS with OCC1N^=_g |
Coffee break | ||
Session 5. Verification | ||
10.00 - 11.00 | Michael Rusinowitch | Compiling and Verifying
Security
Protocols
(invited talk) |
11.00 - 11.30 | Jan Friso Groote,
Jaco van de Pol |
Equational Binary Decision Diagrams |
11.30 - 12.00 | Cecile Canovas-Dumas,
Paul Caspi |
A PVS Proof Obligation Generator for Lustre Programs |
Lunch | ||
Session 6. Logic programming and CLP | ||
14.30 - 15.00 | Roberto Bagnara,
Patricia M. Hill, Enea Zaffanella |
Efficient Structural Information Analysis for Real CLP Languages |
15.00 - 15.30 | Roberto Di Cosmo,
Jean-Vincent Loddo |
Playing Logic Programs with the Alpha-Beta Algorithm |
15.30 - 16.00 | Nikolay Pelov,
Emmanuel De Mot, Marc Denecker |
Logic Programming
Approaches
for Representing and
Solving Constraint Satisfaction Problems: A Comparison |
Coffee break | ||
Session 7. Nonclassical logics and lambda calculus | ||
16.30 - 17.00 | Matthias Baaz,
Agata Ciabattoni, Richard Zach |
Quantified Propositional Goedel Logics |
17.00 - 17.30 | Philippe de Groote | Proof-search in implicative linear logic as a matching problem |
17.30 - 18.00 | Dieter Spreen | A New Model Construction for the Polymorphic Lambda Calculus |
18.00 - 18.30 | Richard Statman | On Church's Lambda Delta Calculus |
Excursion (8:00) |
Session 8. Logic and databases | ||
8.30 - 9.00 | S.Greco,
E. Zumpano |
Querying Inconsistent Databases |
9.00 - 9.30 | I. Horrocks,
U. Sattler, S. Tessaris, S. Tobies |
Query Containment Using a DLR ABox |
Coffee break | ||
Session 9. Program analysis | ||
10.00 - 10.30 | Gilles Barthe,
Bernard Serpette |
Static Reduction Analysis
for
Imperative
Object-Oriented Languages (invited talk) |
10.30 - 11.00 | Roberta Gori | An Abstract
Interpretation approach
to
Termination of Logic Programs |
11.00 - 11.30 | Elvira Albert,
Michael Hanus, German Vidal |
Using an Abstract
Representation
to Specialize
Functional Logic Programs |
11.30 - 12.00 | Wim Vanhoof | Binding-Time Analysis by
Constraint
Solving:
A modular and higher-order approach for Mercury |
Lunch | ||
Session 10. Mu-calculus | ||
14.30 - 15.30 | Erich Grädel | Efficient evaluation
methods
for guarded
logics and Datalog LITE (invited talk) |
15.30 - 16.00 | Jean-Marc Talbot | On the Alternation-free Horn mu-calculus |
Coffee break | ||
Session 11. Planning and reasoning about actions | ||
16.30 - 17.00 | Steffen Hölldobler,
Dietrich Kuske |
The Boundary between
Decidable
and
Undecidable Fragments of the Fluent Calculus |
17.00 - 17.30 | Helko Lehmann,
Michael Leuschel |
Solving Planning Problems by Partial Deduction |
17.30 - 18.00 | Jan Sefranek | A Kripkean Semantics for Dynamic Logic |
Departure for the conference dinner (18:30) |
Conference dinner (19:00) |
A coach will drive us along the coast by the main road towards the south, leaving this road in Saint Louis in order to penetrate the interior of the island by the vertigineous N5 road to Cilaos. We shall reach Cilaos (1200m above sea level) after a ride of 2 hours. Then we split into three groups.
Total ascent | 200m |
Total descent | 450m |
Total acent | 300m |
Total descent | 650m |