| 8.30 | Invited Speaker: Colin Stirling (University of Edinburgh):
|
| -- Decision Procedures for Pushdown Automata
|
| 9.30 | Break
|
| 9.45 | Equational Termination by Semantic Labelling
|
| -- Hitoshi Ohsaki, Aart Middeldorp and Juergen Giesl
|
| 10.15 | Definability over Linear Constraints
|
| -- Michael Benedikt and H. Jerome Keisler
|
| 10.45 | Coffee break
|
| 11.15 | Completeness of Higher-Order Duration Calculus
|
| -- Zhan Naijun
|
| 11.45 | From Programs to Games: Invariance and Safety for Bisimulation
|
| -- Marc Pauly
|
| 12.30 | Lunch, Nature
|
| 15.30 | Flatness is not a Weakness
|
| -- Hubert Comon and Veronique Cortier
|
| 16.00 | On the Complexity of Explicit Modal Logics
|
| -- Roman Kuznets
|
| 16.30 | Coffee break
|
| 17.00 | Modal Satisfiability is in Deterministic Linear Space
|
| -- Edith Hemaspaandra
|
| 17.30 | Independence: Logics and Concurrency
|
| -- J. C. Bradfield
|
| 19.00 | Dinner
|
| 8.30 | Invited Speaker: Paul Beame (University of Washington):
|
| -- The Complexity of Proving Properties of Random Objects
|
| 9.30 | Break
|
| 9.45 | Discreet Games, Light Affine Logic and PTIME Computation
|
| -- A. S. Murawski and C.-H. L. Ong
|
| 10.15 | On the Complexity of Combinatorial and Metafinite Generating Functions
|
| -- J. A. Makowski and K. Meer
|
| 10.45 | Coffee break
|
| 11.15 | The Descriptive Complexity of the Fixed-Points of Bounded Formulas
|
| -- Albert Atserias
|
| 11.45 | Bounded Arithmetic and Descriptive Complexity
|
| -- Achim Blumensath
|
| 12.30 | Lunch, Nature
|
| 15.30 | A Proof-Theoretically Adequate Axiomatization of Intuitionistic Fuzzy Logic
|
| -- Matthias Baaz and Richard Zach
|
| 16.00 | On the Logic of the Standard Proof Predicate
|
| -- Rostislav Yavorsky
|
| 16.30 | Coffee break
|
| 17.00 | Elementary Choiceless Constructive Analysis
|
| -- Peter M. Schuster
|
| 17.30 | A Theory of Explicit Mathematics Equivalent to ID_1
|
| -- Reinhard Kahle and Thomas Studer
|
| 18.15 | EACSL membership meeting
|
| 19.00 | Dinner
|
| | Invited Speakers:
|
| 8.30 | Yuri Gurevich (Microsoft Research, Redmond):
|
| -- On Abstract State Machines
|
| 9.30 | Break
|
| 9.45 | Egon Börger (University of Pisa, on sabbatical at Microsoft Research, Redmond):
|
| -- Composition and Submachine Concepts for Sequential ASMs
|
| 10.45 | Coffee break
|
| 11.15 | Wolfram Schulte (Microsoft Research, Redmond):
|
| -- Translating Theory into Practice - Abstract State Machines within Microsoft
|
| 12.30 | Lunch, Nature
|
| 15.00 | Andreas Blass (University of Michigan, Ann Arbor):
|
| -- On Choiceless Polynomial Time Computation and the Zero-One Law
|
| 16.00 | Coffee break
|
| 16.30 | Moshe Y. Vardi (Rice University, Houston):
|
| -- Automated Verification = Graphs, Automata, and Logic
|
| 17.45 | Saharon Shelah (The Hebrew University, Jerusalem):
|
| -- Choiceless Polynomial Time Logic: Inability to express.
|
| 19.30 | Conference dinner
|
| 8.30 | Invited Speaker: Bruno Poizat (University of Lyon):
|
| -- An unsuccessful attempt to
construct a structure with fast elimination of quantifiers
|
| 9.30 | Break
|
| 9.45 | Finite Models and Full Completeness
|
| -- James Laird
|
| 10.15 | A Fully Complete PER Model for ML Polymorphic Types
|
| -- Samson Abramsky and Marina Lenisa
|
| 10.45 | Coffee break
|
| 11.15 | Logical Relations and Data Abstraction
|
| -- John Power and Edmund Robinson
|
| 11.45 | Sequents, Frames, and Completeness
|
| -- Thierry Coquand and Guo-Quiang Zhang
|
| 12.30 | Lunch
|
| 15.30 | On the Computational Interpretation of Negation
|
| -- Michel Parigot
|
| 16.00 | Logic Programming and Co-inductive Definitions
|
| -- Mathieu Jaume
|
| 16.30 | Coffee break
|
| 17.00 | Axiomatizing the Least Fixed Point Operation and Supremum
|
| -- Zoltan Esik
|
| 17.30 | Disjunctive Tautologies as Synchronization Schemes
|
| -- Vincent Danos and Jean-Louis Krivine
|
| 19.00 | Dinner
|