Logic for Programming and Automated Reasoning

Reunion Island, 
November 6-10, 2000


Monday, November 6

Session 1. Nonmonotonic reasoning
 11:00 - 12.00   Georg Gottlob  Theory Curbing and its Complexity 
 (invited talk)
 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)

Tuesday, November 7

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

Wednesday, November 8

 Excursion (8:00)

Thursday, November 9

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


Social programme

The details will be given later

Welcoming dinner


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.

The conference dinner will take place at Lycée Hôtelier la Renaissance (Plateau Cailloux, Saint Paul). The meal, which will be prepared and served by the pupils, will illustrate the cultural diversity to be found in La Réunion.

Back to the LPAR'2000 homepage