Schedule

June 3, Sunday

7:00pm-9:00pm Welcome party
(free for registered participants)		 O’Reilly’s
21 West 35th Street

June 4, Monday

8:30am-9:00am Registration Lobby of the CUNY GC Auditorium
9:00am-10:00am Plenary talk: The Four Colour Theorem: Engineering of a Formal Proof. Georges Gonthier (Microsoft Research Cambridge)
10:00am-10:30am Coffee
10:30am-11:00am Compactness Properties for Stable Semantics of Logic Programs. Victor Marek (University of Kentucky) and Jeffrey Remmel (University of California San Diego)
11:00 am-11:30am Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking. Raffaella Gentilini (University of Kaiserslautern), Klaus Schneider (TU Kaiserslautern), and Bud Mishra (New York University).
11:30am-12:00pm A Synthesis Algorithm for Hybrid Systems. Srikanth Gottipati (City University of New York) and Anil Nerode (Cornell University).
12:00pm-2:00pm Lunch No organization for this, there will be a list of local lunch places distributed.
2:00pm-2:30pm Weighted O-Minimal Hybrid Systems Are More Decidable Than Weighted Timed Automata! Patricia Bouyer, Thomas Brihaye, and Fabrice Chevalier (LSV – CNRS & ENS de Cachan).
2:30pm-3:00pm Elementary Differential Calculus on Discrete and Hybrid Structures. Howard Blair, David Jakel, Robert Irwin, and Angel Rivera (Syracuse University).
3:00pm-3:30pm A Temporal Dynamic Logic for Verifying Hybrid System Invariants. André Platzer (University of Oldenburg).
3:30pm-4:00pm On the Constructive Dedekind Reals. Robert Lubarsky (Florida Atlantic University) and Michael Rathjen (University of Leeds).
4:00pm-4:30pm Coffee
4:30pm-6:30pm Nerode Special Session. Invited Speakers: Victor Marek and Jeff Remmel.
7:00pm-10:00pm Conference banquet Jewel of India
15 West 44th Street

June 5, Tuesday

9:00am-9:30am Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. Robert Constable and Wojciech Moczydłowski (Cornell University).
9:30am-10:00am Realizations and LP. Melvin Fitting (City University of New York).
10:00am-10:30am Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic. Michael O’Connor (Cornell University).
10:30am-10:45am Coffee
10:45am-11:15am Justified and Common Knowledge: Limited Conservativity. Evangelia Antonakos (City University of New York).
11:15am-11:45am (n,k)-ary Quantifiers in Canonical Systems. Arnon Avron and Anna Zamansky (Tel Aviv University).
11:45am-12:15pm Explicit Proofs in Formal Provability Logic. Evan Goris (City University of New York).
12:15pm-2:00pm Lunch No organization for this, there will be a list of local lunch places distributed.
2:00pm-2:30pm The Law of the Iterated Logarithm for Algorithmically Random Brownian Motion. Bjørn Kjos-Hanssen and Anil Nerode (Cornell University).
2:30pm-3:00pm Some Puzzles about Probability and Probabilistic Conditionals. Rohit Parikh (City University of New York).
3:00pm-3:30pm Verifying Balanced Trees. Zohar Manna, Henny Sipma (Stanford University), and Ting Zhang (Microsoft Research Asia)
3:30pm-3:45pm Coffee
3:45pm-4:15pm Cut Elimination in Deduction Modulo by Abstract Completion. Guillaume Burel (Université Nancy 1 – LORIA) and Claude Kirchner (INRIA – LORIA).
4:15pm-4:45pm Hypersequent Calculus for Intuitionistic Logic with Classical Atoms. Hidenori Kurokawa (City University of New York).
4:45pm-5:15pm Density Elimination and Rational Completeness for First-Order Logics. Agata Ciabattoni (Vienna University of Technology) and George Metcalfe (Vanderbilt University).
5:15pm-6:00pm LFCS Town Meeting

June 6, Wednesday

9:00am-9:30am Total Public Announcements. David Steiner and Thomas Studer (University of Bern).
9:30am-10:00am Reasoning about Sequences of Memory States. Rémi Brochenin, Stéphane Demri, and Étienne Lozes (ENS de Cachan).
10:00am-10:30am Model Checking Knowledge and Linear Time: PSPACE cases. Kai Engelhardt, Peter Gammie, and Ron van der Meyden (University of New South Wales, Australia).
10:30am-10:45am Coffee
10:45am-11:15am Decidable Temporal Logic with Repeating Values. Stéphane Demri (LSV, ENS de Cachan), Deepak D’Souza (IISC, Bangalore), and Régis Gascon (LSV, ENS de Cachan).
11:15am-11:45am Including the Past in ‘Topologic’. Bernhard Heinemann (FernUniversität in Hagen).
11:45am-12:15pm On Decidability and Expressiveness of Propositional Interval Neighborhood Logics. Davide Bresolin (Università degli Studi di Udine), Valentin Goranko (University of the Witwatersrand), Angelo Montanari (Università degli Studi di Udine), and Guido Sciavicco (University of Murcia).
12:15pm-2:00pm Lunch No organization for this, there will be a list of local lunch places distributed.
2:00pm-2:30pm The Intensional Lambda Calculus. Sergei Artemov (City University of New York) and Eduardo Bonelli (National University of Argentina).
2:30pm-3:00pm Uniform Circuits, & Boolean Proof Nets. Virgile Mogbil and Vincent Rahli (Université Paris 13).
3:00pm-3:30pm Multiplexor Categories and Models of Soft Linear Logic. Brian Redmond (University of Ottawa).
3:30pm-4:00pm Coffee
4:00pm-4:30pm Weighted Distributed Systems and Their Logics. Benedikt Bollig (ENS de Cachan) and Ingmar Meinecke (Universität Leipzig).
4:30pm-5:00pm On Complexity of Ehrenfeucht-Fraïssé Games. Bakhadyr Khoussainov and Jiamou Liu (The University of Auckland).
5:00pm-5:30pm Finite Automata Presentable Abelian Groups. André Nies and Pavel Semukhin (The University of Auckland).

June 7, Thursday

9:00am-9:30am Proof Identity for Classical Logic: Generalizing to Normality. Roman Kuznets (City University of New York).
9:30am-10:00am Topological Semantics and Bisimulations for Intuitionistic Modal Logics, and their Classical Companion Logics. Jen Davoren (The University of Melbourne).
10:00am-10:30am The Universal Modality, the Center of a Heyting Algebra, and the Blok-Esakia Theorem. Guram Bezhanishvili (New Mexico State University).
10:30am-11:00am Coffee
11:00am-12:00pm Plenary talk: Natural Proofs: Ten Years After. Alexander Razborov (IAS Princeton and Steklov Institute Moscow)
12:00pm-12:10pm Closure