Schedule of Papers and Events

Summary

Morning Afternoon Evening
Thursday, 1st Registration
Friday, 2nd Conference
ESHOL workshop 		Conference
ESHOL workshop 		Reception
Saturday, 3rd Conference Conference Banquet
Sunday, 4th Conference Conference Dinner party
Monday, 5th Conference Excursion
Tuesday, 6th Conference Conference LPARty

Note: The ESHOL workshop is open to everyone.

Locations

Thursday, 1st December

Registration desk
4:00pm‑6:00pm Registration and information, in the secretariat room

Friday, 2nd December

Registration desk
8:00am‑6:00pm Registration and information, in the secretariat room
 
Session 1 - Constraints - Chair: Bernhard Beckert
9:00am‑9:30am A New Constraint Solver for 3-D Lattices and its Application to the Protein Folding Problem
Alessandro Dal Palù, Agostino Dovier and Enrico Pontelli
9:30am‑10:00am Disjunctive Constraint Lambda Calculi
Matthias Hölzl and John Newsome Crossley
 
ESHOL session 1 - Chair: Christoph Benzmüller
9:00am‑10:00am Invited talk: First Order Proof for Higher Order Logic Theorem Provers
Joe Hurd
 
10:00am‑10:30am Break
 
Session 2 - Logic Programming - Chair: Daniel Dougherty
10:30am‑11:00am Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees
Yao Wu, Enrico Pontelli and Desh Ranjan
11:00am‑11:30am The nomore++ Approach to Answer Set Solving
Christian Anger, Martin Gebser, Thomas Linke, Andre Neumann and Torsten Schaub
11:30am‑12:00am Optimizing the runtime processing of types in logic programming languages
Gopalan Nadathur and Xiaochu Qi
12:00am‑12:30am Extensional Higher-Order Datalog
Vassilis Kountouriotis, Panos Rondogiannis and William Wadge
Deciding Weak Monadic Second-order Logics using Complex-value Datalog
Gulay Unel and David Toman
 
ESHOL session 2 - Chair: Chad Brown
10:30am‑11:00am Implicit Typing in Lambda Logic
Michael Beeson
11:00am‑11:30am LEO - A Resolution based Higher Order Theorem Prover
Christoph Benzmüller
11:30am‑12:00am Combining Proofs of Higher-Order and First-Order Automated Theorem Provers
Christoph Benzmüller, Volker Sorge, Mateja Jamnik and Manfred Kerber
12:00am‑12:30am Vacant
 
12:30pm‑1:30pm Lunch, in the restaurant
 
Session 3 - Logical Foundations of Programming - Chair: John Crossley
1:30pm‑2:00pm The Four Sons of Penrose
Nachum Dershowitz
2:00pm‑2:30pm An Algorithmic Account of Winning Strategies in Ehrenfeucht Games on Labeled Successor Structures
Angelo Montanari, Alberto Policriti and Nicola Vitacolonna
2:30pm‑3:00pm Second-Order Principles in Specification Languages for Object-Oriented Programs
Bernhard Beckert and Kerry Trentelman
3:00pm‑3:30pm Strong Normalization of the Dual Classical Sequent Calculus
Daniel Dougherty, Silvia Ghilezan, Pierre Lescanne and Silvia Likavec
 
ESHOL session 3 - Chair: Michael Beeson
1:30pm‑2:30pm Invited talk: Benchmarks for Higher-Order Automated Reasoning
Chad Brown
2:30pm‑3:00pm Co-Synthesis of New Complex Selection Algorithms and their Human Comprehensible XML Documentation
Jutta Eusterbrock
3:00pm‑3:30pm Mixing Finite Success and Finite Failure in an Automated Prover
Alwen Tiu, Gopalan Nadathur and Dale Miller
 
3:30pm‑4:00pm Break
 
Session 4 - Rewriting - Chair: Hitoshi Ohsaki
4:00pm‑4:30pm Termination of Fair Computations in Term Rewriting
Salvador Lucas and José Meseguer
4:30pm‑5:00pm On Confluence of Infinitary Combinatory Reduction Systems
Jeroen Ketema and Jakob Grue Simonsen
5:00pm‑5:30pm Matching with Regular Constraints
Temur Kutsia and Mircea Marin
5:30pm‑6:00pm Recursive Path Orderings can also be Incremental
Mirtha-Lina Fernandez, Guillem Godoy and Albert Rubio
 
ESHOL session 4 - Chair: Christoph Benzmüller
4:00pm‑5:00pm System Demonstrations
Otter-λ Michael Beeson, TPS Chad Brown, Metis Joe Hurd, LEO Christoph Benzmüller
5:00pm‑6:00pm Panel: A Higher-Order TPTP - Feasible or Not?
 
6:00pm‑9:00pm Reception, in the Gary Room and on the terrace
  • Snacks and drinks
  • Welcoming address by Honorable Minister Phillip Paulwell of the Ministry of Commerce, Science and Technology.
  • Sponsored by Wray and Nephew.

    • Saturday, 3rd December

    Registration desk
    8:00am‑6:00pm Registration and information, in the secretariat room
     
    Session 5 - Chair: Geoff Sutcliffe
    9:00am‑10:00am Invited talk: Independently Checkable Proofs from Decision Procedures: Issues and Progress
    Allen Van Gelder
     
    10:00am‑10:30am Break
     
    Session 6 - Automated Reasoning - Chair: Jeff Pelletier
    10:30am‑11:00am Automating Coherent Logic
    Marc Bezem and Thierry Coquand
    11:00am‑11:30am The Theorema Environment for Interactive Proof Development
    Florina Piroi and Temur Kutsia
    11:30am‑12:00am A First Order Extension of Stalmarck's Method
    Magnus Björk
    12:00am‑12:30am Regular Derivations in Basic Superposition-Based Calculi
    Vladimir Aleksic and Anatoli Degtyarev
     
    12:30pm‑1:30pm Lunch, in the restaurant
     
    Session 7 - Decision Procedures - Chair: Marc Bezem
    1:30pm‑2:00pm On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity
    Lidia Tendera and Wieslaw Szwast
    2:00pm‑2:30pm Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
    Chao Wang, Aarti Gupta, Franjo Ivancic and Malay Ganai
    2:30pm‑3:00pm Monotone AC-Tree Automata
    Hitoshi Ohsaki, Jean-Marc Talbot, Yves Roos and Sophie Tison
    3:00pm‑3:30pm On the Specification of Sequent Systems
    Elaine Pimentel and Dale Miller
     
    3:30pm‑4:00pm Break
     
    Session 8 - Systems and Implementations - Chair: Temur Kutsia
    4:00pm‑4:30pm Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
    Amine Chaieb and Tobias Nipkow
    4:30pm‑5:00pm Integration of a Software Model Checker into Isabelle
    Matthias Daum, Stefan Maus, Norbert Schirmer and Mohamed Nassim Seghir
    5:00pm‑5:30pm A SAT-based Sudoku Solver
    Tjark Weber
    Matchmaking and Personalization on Mobile Devices
    Thomas Kleemann and Alex Sinner (Bernhard Beckert)
    5:30pm‑6:00pm Vacant
     
    7:00pm Banquet, at the Groovy Grouper, in Drs Cave Beach
  • Jamaican dinner and drinks on the beach.

    • Sunday, 4th December

    Registration desk
    8:00am‑6:00pm Registration and information, in the secretariat room
     
    Session 9 - Chair: Andrei Voronkov
    9:00am‑10:00am Invited talk: Zap: Automated Theorem Proving for Software Analysis
    Tom Ball
     
    10:00am‑10:30am Break
     
    Session 10 - Verification I - Chair: Tom Ball
    10:30am‑11:00am Experimental Evaluation of Classical Automata Constructions
    Deian Tabakov and Moshe Vardi
    11:00am‑11:30am Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics
    Wolfgang Ahrendt, Andreas Roth and Ralf Sasse
    11:30am‑12:00am Reasoning about Incompletely Defined Programs
    Christoph Walther and Stephan Schweitzer
    12:00am‑12:30am Model Checking Abstract State Machines with Answer Set Programming
    Calvin Kai Fan Tang and Eugenia Ternovska
     
    12:30pm‑1:30pm Lunch, in the restaurant
     
    Session 11 - Verification II - Chair: Annabelle McIver
    1:30pm‑2:00pm Characterizing Provability in BI's Pointer Logic through Resource Graphs
    Didier Galmiche and Daniel Méry
    2:00pm‑2:30pm A Unified Memory Model for Pointers
    Harvey Tuch and Gerwin Klein
    2:30pm‑3:00pm Treewidth in Verification: Local vs. Global
    Andrea Ferrara, Guoqiang Pan and Moshe Vardi
    3:00pm‑3:30pm Pushdown Module Checking
    Laura Bozzelli, Aniello Murano and Adriano Peron
     
    3:30pm‑4:00pm Break
     
    Session 12 - Verification III - Chair: Wolfgang Ahrendt
    4:00pm‑4:30pm Functional Correctness Proofs of Encryption Algorithms
    Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind and Junxing Zhang
    4:30pm‑5:00pm Towards Automated Proof Support for Probabilistic Distributed Systems
    Annabelle McIver and Tjark Weber
    5:00pm‑5:30pm Algebraic Intruder Deductions
    David Basin, Sebastian Mödersheim and Luca Viganòio
    5:30pm‑6:00pm A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela+
    Florian Rabe, Steffen Schlager and Peter Schmitt
    Vacant
     
    7:00pm Dinner Party, at the Pork Pit
  • Dinner and drinks at a local jerk center

    • Monday, 5th December

    Registration desk
    8:00am‑6:00pm Registration and information, in the secretariat room
     
    Session 13 - Chair: Geoff Sutcliffe
    9:00am‑10:00am Invited talk: Decision procedures for SAT, SAT Modulo Theories and Beyond - The BarcelogicTools
    Roberto Nieuwenhuis
     
    10:00am‑10:30am Break
     
    Session 14 - Satisfiability Checking - Chair: Roberto Nieuwenhuis
    10:30am‑11:00am Satisfiability Checking for PC(ID)
    Maarten Mariën, Rudradeb Mitra, Marc Denecker and Maurice Bruynooghe
    11:00am‑11:30am Pool Resolution and its Relation to Regular Resolution and DPLL with Clause Learning
    Allen Van Gelder
    11:30am‑12:00am Another Complete Local Search Method for SAT
    Hantao Zhang and Haiou Shen
    12:00am‑12:30am Designing Efficient Procedures for #2SAT
    Guillermo De Ita, Mireya Tovar, Erica Vera and Carlos Guillén
    Exploring Hybrid Algorithms for SAT
    Olivier Fourdrinoy, Eric Gregoire, Bertrand Mazure and Sais Lakhdar
     
    12:30pm‑1:30pm Lunch, in the restaurant
     
    1:30pm Excursion (optional extra). A choice of:
  • Rafting the Great River with Caliche (choice of gentle rainforest rafting or bumpy whitewater rafting)
  • A (slightly wild) ride through the Jamaican rainforest canopy with Chukka Blue
  • Lazing on the beach at Doctors Cave Bathing Club

    • Tuesday, 6th December

    Registration desk
    8:00am‑6:00pm Registration and information, in the secretariat room
     
    Session 15 - Chair: Andrei Voronkov
    9:00am‑10:00am Invited talk: Scaling Up: Computers vs. Common Sense
    Doug Lenat
     
    10:00am‑10:30am Break
     
    Session 16 - Knowledge Representation - Chair: Nicola Olivetti
    10:30am‑11:00am Inference from Controversial Arguments
    Sylvie Coste-Marquis, Caroline Devred and Pierre Marquis
    11:00am‑11:30am Programming Cognitive Agents in Defeasible Logic
    Mehdi Dastani, Guido Governatori, Antonino Rotolo and Leendert van der Torre
    11:30am‑12:00am The Relationship between Reasoning about Privacy and Default Logics
    Jürgen Dix, Wolfgang Faber and V.S Subrahmanian
    12:00am‑12:30am Fregean Albebraic Tableaux: Automating Inferences in Fuzzy Propositional Logic
    Francis Jeffry Pelletier and Christopher Lepock
    A Logical Language for Dominoes
    Fernando Raymundo Velázquez-Quesada and Francisco Hernández-Quiroz
     
    12:30pm‑1:30pm Lunch, in the restaurant
     
    Session 17 - Non-classical Logic - Chair: Lidia Tendera
    1:30pm‑2:00pm Comparative Similarity, Tree Automata, and Diophantine Equations
    Mikhail Sheremet, Dmitry Tishkovsky, Frank Wolter and Michael Zakharyaschev
    2:00pm‑2:30pm Analytic Tableaux for KLM Preferential and Cumulative Logics
    Laura Giordano, Valentina Gliozzi, Nicola Olivetti and Gian Luca Pozzato
    2:30pm‑3:00pm Bounding Resource Consumption with Gödel-Dummett Logics
    Dominique Larchey-Wendling
    3:00pm‑3:30pm On interpolation in Existence Logics
    Matthias Baaz and Rosalie Iemhoff
     
    3:30pm‑4:00pm Break
     
    Session 18 - Non-classical Reasoning - Chair: Matthias Baaz
    4:00pm‑4:30pm Incremental Integrity Checking: Limitations and Possibilities
    Henning Christiansen and Davide Martinenghi
    4:30pm‑5:00pm Concepts of Automata Construction from LTL
    Carsten Fritz
    5:00pm‑5:30pm Reasoning on Multimodal logic with the Calculus of Inductive Constructions
    Houda Anoun
    A Hierarchical Logic for Network Configuration
    Roger Villemaire, Sylvain Hallé, Omar Cherkaoui and Rudy Deca
    5:30pm‑6:00pm Vacant
     
    7:00pm LPARty, at Pier 1
  • A grand cultural event of RPARs, to balance the LPARs

    • Jamaica ... Land of LPAR and Reggae