LICS 2007 PRELIMINARY PROGRAMME http://www2.informatik.hu-berlin.de/lics/lics07/ (last modified 9 May 2007) ------------------------------------------------------------------------ Tuesday 10 July [Type Theory] 0900 Andreas Abel, Thierry Coquand and Peter Dybjer. Dependent Types with Universes via Normalization-by-Evaluation 0930 Colin Riba. Strong Normalization as Safe Interaction 1000 Wojciech Moczydlowski. A Dependent Set Theory [Security] 1030 Mika Cohen and Mads Dam. A Complete Axiomatization of Knowledge and Cryptography 1100 C O F F E E [Computational Proof Theory] 1130 Paul Brauner, Clément Houtmann and Claude Kirchner. Principles of Superdeduction 1200 James Brotherston and Alex Simpson. Complete Sequent Calculi for Induction and Infinite Descent 1230 SHORT PRESENTATIONS 1 1300 L U N C H 1430 INVITED LECTURE: Tom Hales. The Kepler Conjecture and the Flyspeck Project 1530 LICS AWARDS CEREMONY 1630 C O F F E E [Timed and Stochastic Systems] 1700 Hugo Gimbert and Wieslaw Zielonka. Limits of Multi–Discounted Markov Decision Processes 1730 Luca de Alfaro, Rupak Majumdar, Vishwanath Raman and Marielle Stoelinga. Game Relations and Metrics 1800 Patricia Bouyer, Nicolas Markey, Joel Ouaknine and James Worrell. The Cost of Punctuality 2000 WELCOME RECEPTION ------------------------------------------------------------------------ Wednesday 11 July [Verification] 0900 Rajeev Alur, Marcelo Arenas, Pablo Barcelo, Kousha Etessami, Neil Immerman and Leonid Libkin. First-order and Temporal Logics for Nested Words 0930 Salvatore La Torre, Madhusudan Parthasarathy and Gennaro Parlato. A Robust Class of Context-Sensitive Languages 1000 Francesco Ranzato and Francesco Tapparo. A New Efficient Simulation Equivalence Algorithm 1030 Detlef Kaehler, Ralf Kuesters and Tomasz Truderung. Infinite State AMC-Model Checking for Cryptographic Protocols 1100 C O F F E E 1130 Mikolaj Bojanczyk. Two-way unary temporal logic over trees 1200 Marcin Jurdzinski and Ranko Lazic. Alternation-Free Modal Mu-Calculus for Data Trees 1230 Angelo Montanari and Gabriele Puppis. A Contraction Method to Decide MSO Theories of Trees 1300 L U N C H 1430 EXCURSION ------------------------------------------------------------------------ Thursday 12 July [Constraints] 0900 Laszlo Egri, Benoit Larose and Pascal Tesson. Symmetric Datalog and Constraint Satisfaction Problems in Logspace 0930 Manuel Bodirsky and Hubie Chen. Quantified Equality Constraints 1000 Pawel Idziak, Petar Markovic, Ralph McKenzie, Matt Valeriote and Ross Willard. Tractability and learnability arising from algebras with few subpowers [Proof Complexity] 1030 Steven James Perron. Examining The Fragments of G 1100 C O F F E E 1130 Phuong Nguyen. Separating DAG-Like and Tree-Like Proof Systems 1200 Phuong Nguyen and Stephen A. Cook. The Complexity of Proving the Discrete Jordan Curve Theorem [Finite Model Theory] 1230 Anuj Dawar, Martin Grohe and Stephan Kreutzer. Locally Excluding a Minor 1300 L U N C H 1430 INVITED LECTURE: Phokion Kolaitis. Reflections on Finite Model Theory 1530 Balder ten Cate, Jouko Vaananen and Johan van Benthem. Lindstrom theorems for fragments of first-order logic 1600 C O F F E E [Concurrency and Process Calculus] 1630 Davide Sangiorgi, Naoki Kobayashi and Eijiro Sumii. Environment Bisimulations for Higher-Order Languages 1700 Marcello Bonsangue and Alexander Kurz. Pi-Calculus in Logical Form 1730 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Chenyi Zhang. Characterising Testing Preorders for Finite Probabilistic Processes ------------------------------------------------------------------------ Friday 13 July [Semantics of Programming Languages] 0900 ICALP-LICS INVITED LECTURE: Gordon Plotkin. The Algebraic Theory of Effects 1000 C O F F E E 1030 Bartek Klin. Bialgebraic operational semantics and modal logic 1100 Rasmus Ejlers Mogelberg and Alex Simpson. Relational Parametricity for Computational Effects 1130 Francois Pottier. Static Name Control for FreshML 1200 Cristiano Calcagno, Peter O'Hearn and Hongseok Yang. Local Action and Abstract Separation Logic 1230 L U N C H 1400 ICALP-LICS INVITED LECTURE: Michael Rabin. Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations, and Applications 1500 C O F F E E [Game Semantics] 1530 Paul-André Melliès and Nicolas Tabareau. Resource Modalities in Game Semantics 1600 Nikos Tzevelekos. Full abstraction for nominal general references 1630 SHORT PRESENTATIONS 2 1730 DEGREE CEREMONY (Leopoldinum) 1915 LICS BUSINESS MEETING ------------------------------------------------------------------------ Saturday 14 July [Linear Logic] 0900 Ulrich Schoepp. Stratified Bounded Affine Logic for Logarithmic Space 0930 Patrick Baillot, Paolo Coppola and Ugo Dal Lago. Light Logics and Optimal Reduction: Completeness and Complexity 1000 Paulo Oliva. Modified Realizability Interpretation of Classical Linear Logic 1030 C O F F E E [Joint Session on Logic in Computer Science with Logic Colloquium 2007] 1100 INVITED LECTURE: Martin Hyland. Combinatorics of Proofs 1200 INVITED LECTURE: Rosalie Iemhoff Skolemization in constructive theories 1230 INVITED LECTURE: Alex Simpson Non-well-founded Proofs 1300 L U N C H 1430 INVITED LECTURE: Colin Stirling. Higher-Order Matching, Games and Automata 1530 INVITED LECTURE: Cristiano Calcagno. Can logic tame systems programs? 1600 INVITED LECTURE: Martin Escardo. Infinite sets that admit exhaustive search I 1630 C O F F E E [Topology and Computable Mathematics] 1700 Martin Escardo. Infinite sets that admit exhaustive search II 1730 Jean Goubault-Larrecq. On Noetherian Spaces 1800 Abbas Edalat. A Computable Approach to Measure and Integration Theory ------------------------------------------------------------------------