|
Monday 22 August 2005
|
| 8:30 |
Registration
|
| 9:00 |
Invited lecture: Ulrich Berger. An Abstract Strong Normalization Theorem
|
|
Semantics
and Logics |
10:00 |
Matthew Collinson, David Pym and Edmund Robinson. On Bunched Polymorphism |
| 10:30 |
Coffee |
| 11:00 |
Tom Murphy, Robert Harper and Karl Crary. Distributed Control Flow with Classical Modal
Logic |
| 11:30 |
Jiri Adamek. A Logic of Coequations |
| 12:00 |
Shin-ya Katsumata. A Semantic Formulation of TT-lifting and Logical
Predicates for Computational Metalanguage |
| 12:30 |
Lunch |
|
Type Theory
and Lambda Calculus I |
| 14:00 |
Paula Severi and Fer-Jan de Vries. Order Structures on Boehm-like Models |
| 14:30 |
Colin Stirling. Higher-order Matching and Games |
|
Constructive
Reasoning and Computational Mathematics I |
| 15:00 |
Branimir Lambov. Complexity and Intensionality in a Type-1 Framework for
Computable Analysis |
| 15:30 |
Tea |
| 16:00 |
Vasco Brattka and Matthias Schroeder. Computing with Sequences, Weak Topologies
and the Axiom of Choice |
|
Linear Logic
and Ludics I |
| 16:30 |
Pierre-Louis Curien and Claudia Faggian. L-nets, Strategies and Proof-nets |
| 17:00 |
Jean-Marc Andreoli, Gabriele Pulcini, and Paul Ruet. Permutative Logic |
| 17:30 |
Kaustuv Chaudhuri and Frank Pfenning. Focusing the Inverse Method for Linear
Logic |
|
Evening Event |
| 19:00 |
EACSL Annual
General Meeting, Fitzjames Room 1, Merton College |
| Tuesday 23 August 2005 |
| 9:00 |
Invited lecture: Matthias Baaz.
Proof Theory of Analogical Reasoning and Juridical Logic
|
| Linear Logic and Ludics II |
| 10:00 |
Esfandiar Haghverdi and Philip J. Scott. Towards a Typed Geometry of
Interaction |
| 10:30 |
Coffee |
| Constraints |
| 11:00 | Hubie Chen and Victor Dalmau. From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified
Constraint Satisfaction |
| 11:30 |
Ashish Tiwari. An Algebraic Approach for the Unsatisfiability of Nonlinear
Constraints |
| 12:00 |
Lunch |
| 13:15 |
Depart for Excursion |
| Wednesday 24 August 2005 |
| 9:00 |
Invited lecture: Maarten Marx. XML Navigation and Tarski's Relation
Algebras |
|
Finite
Models, Decidability and Complexity |
| 10:00 |
Marcin Mostowski and Konrad Zdanowski. Coprimality in Finite Models |
| 10:30 |
Coffee |
| 11:00 |
Michael Benedikt and Luc Segoufin. Towards a Characterization of
Order-Invariant Queries over Tame Structures |
| 11:30 |
Bakhadyr Khoussainov and Sasha Rubin. Decidability of Term Algebras Extending
Partial Algebras |
| 12:00 |
Emanuel Kieronski. Results on the Guarded Fragment with Equivalence or
Transitive Relations |
| 12:30 |
Lunch |
| 14:00 |
Bruno Courcelle and Christian Delhomme. The Modular Decomposition of
Countable Graphs: Constructions in Monadic Second-Order Logic |
| 14:30 |
Balder ten Cate and Massiomo Franceschet. On the Complexity of Hybrid Logics
with Binders |
| 15:00 |
Julian Bradfield and Stephan Kreutzer. The Complexity of
Independence-Friendly Fixpoint Logic |
| 15:30 |
Tea |
| 16:00 |
Antonina Kolokolova. Closure properties of weak systems of bounded arithmetic |
|
Ackermann
Award Presentation |
| 16:30 |
Johann Makowsky, Jury Chair |
| 16:45 |
Mikolaj Bojanczyk. Decidable Properties of Tree Languages |
| 17:15 |
Konstantin Korovin. Knuth-Bendix orders in automated deduction and term
rewriting |
|
Evening Event |
| 19:30 |
Conference Banquet, Merton College |
| Thursday 25 August 2005 |
| 9:00 | Invited Lecture: Anatol Slissenko. Verification in Predicate Logic with Time: Algorithmic Questions |
|
Verification
and Model Checking |
| 10:00 |
Julian Bradfield, Jacques Duparc and Sandra Quickert. Transfinite Extension
of the Mu-Calculus |
| 10:30 |
Coffee |
| 11:00 |
Witold Charatonik, Lilia Georgieva and Patrick Maier. Bounded Model Checking
of Pointer Programs |
| 11:30 |
Carsten Lutz. PDL with Intersection and Converse is Decidable |
| 12:00 |
Filip Murlak. On Deciding Topological Classes of Deterministic Tree Languages |
| 12:30 |
Lunch |
|
Type Theory
and Lambda Calculus II |
| 14:00 |
Frederic Blanqui. Decidability of Type-checking in the Calculus of Algebraic
Constructions with Size Annotations |
| 14:30 |
Bruno Barras and Benjamin Gregoire. On the role of type decorations in the
Calculus of Inductive Constructions |
|
Constructive
Reasoning and Computational Mathematics II |
| 15:00 |
Mircea-Dan Hernest. Light Functional Interpretation - an optimization of
Goedel's technique towards the extraction of (more) efficient programs from (classical) proofs |
| 15:30 |
Tea |
| 16:00 |
Michael Soltys. Feasible Proofs of Matrix Properties with Csanky's Algorithm |
|
Implicit
Computational Complexity and Rewriting |
| 16:30 |
Steven Perron. A Propositional Proof System for Log Space |
| 17:00 |
Carsten Schuermann and Jatin Shah. Identifying polynomial-time recursive
functions |
| 17:30 |
Guillem Godoy and Ashish Tiwari. Confluence of Shallow Right-Linear Rewrite
Systems |
