[Home] [Programme] [Timetable] [Venue] [Registration]  Scientific programme

Monday, September 20

Session 1: 9.00 am – 10.15 am
Invited talk: Ken McMillan, Applications of Craig Interpolation to Model Checking
Session 2: 10.45 am – 12.15 pm
Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdzinski, On Nash Equilibria in Stochastic Games
Mikolaj Bojanczyk, A Bounding Quantifier
Hugo Gimbert, Parity and Exploration Games on Infinite Graphs
Session 3: 1.30 pm – 3.00 pm
Harald Ganzinger and Konstantin Korovin, Integrating Equational Reasoning into Instantiation-based Theorem Proving
George Metcalfe, Nicola Olivetti, and Dov Gabbay, Goal-Directed Methods for Lukasiewicz Logic
Jeremy E. Dawson and Rajeev Goré, A General Theorem on Termination of Rewriting
Session 4: 3.30 pm – 5.00 pm
Pierre Hyvernat, Predicate Transformers and Linear Logic: yet another Denotational Model
Pietro Di Gianantonio, Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity
Lutz Straßburger and François Lamarche, On Proof Nets for Multiplicative Linear Logic with Units

Tuesday, September 21

Session 5: 9.00 am – 10.15 am
Invited talk: Pawel Urzyczyn, My (Un)Favourite Things
Session 6: 10.45 am – 12.15 pm
Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv and Greta Yorsh, The Boundary Between Decidability and Undecidability for Transitive Closure Logics
Marcelo Arenas, Pablo Barceló, and Leonid Libkin, Game-based Notions of Locality over Finite Models
Andreas Abel and Ralph Matthes, Fixed Points of Type Constructors and Primitive Recursion
Session 7: 1.30 pm – 3.00 pm
Aleksy Schubert, On the Building of Affine Retractions
Philippe de Groote and Sylvain Salvati, Higher-order Matching in the Linear λ-calculus with Pairing
Ulrich Schöpp and Ian Stark, A Dependent Type Theory with Names and Binding
Session 8: 3.30 pm – 5.00 pm
Tjark Weber, Towards Mechanized Program Verification with Separation Logic
Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, and Line Jakubiec, A Functional Scenario for Bytecode Verification of Resource Bounds
Roberto Giacobazzi and Isabella Mastroeni, Proving Abstract Non-Interference

Wednesday, September 22

Session 9: 9.00 am – 10.15 am
Invited talk: Dale Miller, Bindings, mobility of bindings, and the ∇-quantifier
Session 10: 10.45 am – 12.15 pm
Patrick Maier, Intuitionistic LTL and a New Characterization of Safety and Liveness
Philipp Rohde, Moving in a Crumbling Network: The Balanced Case
E. Allen Emerson and Vineet Kahlon, Parameterized Model Checking of Ring-based Message Passing Systems

Thursday, September 23

Session 11: 9.00 am – 10.15 am
Invited talk: Martin Hyland, Abstract Interpretation of Proofs: Classical Propositional Logic
Session 12: 10.45 am – 12.15 pm
Alan Skelley, A Third-Order Bounded Arithmetic Theory for PSPACE
Andrés Cordón-Franco, Alejandro Fernández-Margarit, and F. Félix Lara-Martín, Provably Total Primitive Recursive Functions: Theories with Induction
David Richerby, Logical Characterizations of PSPACE
Session 13: 1.30 pm – 3.00 pm
Lutz Schröder, The Logic of the Partial λ-Calculus With Equality
Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang, Complete Lax Logical Relations for Cryptographic Lambda-Calculi
Jérôme Vouillon, Subtyping Union Types
Session 14: 3.30 pm – 5.00 pm
Margarita Korovina and Nicolai Vorobjov, Pfaffian Hybrid Systems
Yukiyoshi Kameyama, Axioms for Delimited Continuations in the CPS Hierarchy
Pawel Rychlikowski and Tomasz Truderung, Set Constraints on Regular Terms

Friday, September 24

Session 15: 9.00 am – 10.15 am
Invited talk: Albert Atserias, Notions of Average-Case Complexity for Random 3-SAT
Session 16: 10.45 am – 12.15 pm
Christopher Lynch, Unsound Theorem Proving
Alessandro Avellone, Camillo Fiorentini, Guido Fiorino, and Ugo Moscato, An Efficent Implementation of a Tableau Calculus for a Logic with a Constructive Negation
Agata Ciabattoni, Automated Generation of Analytic Calculi for Logics with Linearity

0
0
Last modified: Jul 15, 2004, 18:59