Symposium Program

08:00-09:00 - LOPSTR/PPDP/SAS Registration

08:45-09:00 - Welcome to LOPSTR 2016

• Manuel Hermenegildo, Pedro López-García, and James Cheney

09:00-10:00 - Invited talk (jointly with PPDP) (Chair: James Cheney)

• Greg Morrisett, Cornell University, USA
  Challenges in Compiling Coq.

10:30-12:00 - Program transformation (Chair: Jérôme Feret)

• Partial Evaluation of Order-sorted Equational Programs modulo Axioms.
  María Alpuente, Angel Cuenca, Santiago Escobar, and Jose Meseguer.
• A Formal, Resource Consumption-Preserving Translation of Actors to Haskell.
  Elvira Albert, Nikolaos Bezirgiannis, Frank De Boer, and Enrique Martin-Martin.
• Verification of Time-Aware Business Processes using Constrained Horn Clauses.
  Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi, and Maurizio Proietti.

13:30-14:30 - Constraint programming (Chair: Manuel Carro)

• MiniZinc with Strings.
  Roberto Amadini, Pierre Flener, Justin Pearson, Joseph D. Scott, Peter J. Stuckey, and Guido Tack.
• Slicing Concurrent Constraint Programs.
  Moreno Falaschi, Maurizio Gabbrielli, Carlos Olarte, and Catuscia Palamidessi.

Excursion and PPDP/LOPSTR Dinner (Royal College of Surgeons)

08:00-09:00 - LOPSTR/PPDP/SAS Registration

09:00-10:00 - Invited talk (jointly with PPDP) (Chair: Pedro López-García)

• Francesco Logozzo, Facebook, USA
  Static analysis for security at the Facebook scale.

10:30-12:00 - Compilation and optimization (Chair: Moreno Falaschi)

• A New Functional-Logic Compiler for Curry: Sprite.
  Sergio Antoy and Andy Jost.
• lpopt: A Rule Optimization Tool for Answer Set Programming.
  Manuel Bichler, Michael Morak, and Stefan Woltran.
• Tuning Fuzzy Logic Programs with Symbolic Execution.
  Ginés Moreno, Jaime Penabad, and Germán Vidal.

13:30-15:00 - Analysis and verification (Chair: Jorge A. Navas)

• Hierarchical Shape Abstraction of Free-List Memory Allocators.
  Bin Fang and Mihaela Sighireanu.
• A Productivity Checker for Logic Programming.
  Ekaterina Komendantskaya, Patricia Johann and Martin Schmidt.
• Symbolic Abstract Contract Synthesis in a Rewriting Framework.
  María Alpuente, Daniel Pardo, and Alicia Villanueva.

15:30-17:00 - Testing (Chair: Patricia Hill)

• On the Completeness of Selective Unification in Concolic Testing of Logic Programs.
  Fred Mesnard, Etienne Payet, and Germán Vidal.
• CurryCheck: Checking Properties of Curry Programs.
  Michael Hanus.
• A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms (best paper award).
  Paul Tarau.

08:00-09:00 - LOPSTR/SAS Registration

09:00-10:00 - Invited talk (jointly with SAS) (Chair: Manuel Hermenegildo)

• Martin Vechev, ETH Zurich, Switzerland
  Learning from Programs: Probabilistic Models, Program Analysis and Synthesis.

10:30-12:00 - Semantics and model checking (Chair: Maurizio Proietti)

• Towards Reversible Computation in Erlang.
  Naoki Nishida, Adrián Palacios, and Germán Vidal.
• Scaling Bounded Model Checking By Transforming Programs With Arrays.
  Anushri Jana, Uday Khedker, Advaita Datar, R Venkatesh, and C. Niyas
• Intuitionistic Logic Programming for SQL.
  Fernando Sáenz-Pérez.

13:30-15:00 - Types, unification, and logic (Chair: Paul Tarau)

• Coinductive Soundness of Corecursive Type Class Resolution.
  Frantisek Farka, Ekaterina Komendantskaya, Kevin Hammond, and Peng Fu.
• Nominal Unification of Higher Order Expressions with Recursive Let.
  Manfred Schmidt-Schauss, Temur Kutsia, Jordi Levy, and Mateu Villaret.
• Automata Theory Approach to Predicate Intuitionistic Logic.
  Maciej Zielenkiewicz and Aleksy Schubert.