[Termtools] CICLOPS-WLPE 2014: CALL FOR PARTICIPATION

Thomas Ströder stroeder at informatik.rwth-aachen.de
Thu Jun 5 16:14:44 CEST 2014


Apologies for multiple copies. Please forward to interested
colleagues.

------------------------------------------------------------
          CICLOPS-WLPE 2014: CALL FOR PARTICIPATION

International Joint Workshop on Implementation of Constraint
   and Logic Programming Systems and Logic-based Methods in
                Programming Environments 2014

                     July 17-18,  2014
                      Vienna, Austria
               http://vsl2014.at/ciclops-wlpe/
------------------------------------------------------------

Keynote Talks:
CICLOPS-WLPE 2014 includes two keynote talks (plus one more
by CHR - see note on joint program below).

Michael Codish, Luís Cruz-Filipe, Michael Frank and Peter
Schneider-Kamp
Proofs for Optimality of Sorting Networks by Logic
Programming

We present a computer-assisted non-existence proof of
nine-input sorting networks consisting of 24 comparators,
hence showing that the 25-comparator sorting network found
by Floyd in 1964 is optimal. As a corollary, we obtain that
the 29-comparator network found by Waksman in 1969 is
optimal when sorting ten inputs. This closes the two
smallest open instances of the optimal size sorting network
problem, which have been open since the results of Floyd and
Knuth from 1966 proving optimality for sorting networks of
up to eight inputs. The entire implementation is written in
SWI-Prolog and was run on a cluster of 12 nodes with 12
cores each, able to run a total of 288 concurrent threads,
making extensive use of SWI-Prolog’s built-in predicate
concurrency/3. The search space of 2.2×10 37 comparator
networks was exhausted after just under 10 days of
computation. This shows the ability of logic programming to
provide a scalable parallel implementation while at the same
time instilling a high level of trust in the correctness of
the proof.


Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian
Emmes and Carsten Fuhs
Symbolic Evaluation Graphs and Term Rewriting - A General
Methodology for Analyzing Logic Programs

There exist many powerful techniques to analyze termination
and complexity of term rewrite systems (TRSs). Our goal is
to use these techniques for the analysis of other
programming languages as well. For instance, approaches to
prove termination of definite logic programs by a
transformation to TRSs have been studied for decades.
However, a challenge is to handle languages with more
complex evaluation strategies (such as Prolog, where
predicates like the cut influence the control flow).
   We present a general methodology for the analysis of such
programs. Here, the logic program is first transformed into
a symbolic evaluation graph which represents all possible
evaluations in a finite way. Afterwards, different analyses
can be performed on these graphs. In particular, one can
generate TRSs from such graphs and apply existing tools for
termination or complexity analysis of TRSs to infer
information on the termination or complexity of the original
logic program.


Workshop Program:

Thursday, July 17th
08:45-10:15 Invited Talk I
Michael Codish, Luís Cruz-Filipe, Michael Frank and Peter
Schneider-Kamp
Proofs for Optimality of Sorting Networks by Logic
Programming
10:15-10:45 Coffee Break
10:45-13:00 Program Transformation
10:45	
Joachim Jansen and Gerda Janssens
Refining definitions with unknown opens using XSB for IDP3
11:15	
Gopalan Nadathur and Mary Southern
A Lambda Prolog Based Animation of Twelf Specifications
11:45	
Md Solimul Chowdhury and Jia-Huai You
A System for Embedding Global Constraints into SAT
12:15	
Jose F. Morales and Manuel V. Hermenegildo
Towards Pre-Indexed Terms
13:00-14:30 Lunch Break
14:30-16:00 Prolog Extensions
14:30	
Vincent Bloemen, Daniel Diaz, Machiel van der Bijl and
Salvador Abreu
Extending the Finite Domain Solver of GNU Prolog
15:00	
Jan Wielemaker
SWI-Prolog version 7 extensions
15:30	
Theofrastos Mantadelis and Ricardo Rocha
A Portable ISO Predicate for Printing Rational Terms
16:00-16:30 Coffee Break
16:30-18:00 Joint with PLP: Perspectives

Friday, July 18th
08:45-10:15 CHR I
10:15-10:45 Coffee Break
10:45-13:00 CHR II
13:00-14:30 Lunch Break
14:30-16:00 Invited Talk II
Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian
Emmes and Carsten Fuhs
Symbolic Evaluation Graphs and Term Rewriting - A General
Methodology for Analyzing Logic Programs
16:00-16:30 Coffee Break
16:30-18:00 Implementation Issues
16:30	
Alexei A. Morozov and Alexander F. Polupanov
Intelligent Visual Surveillance Logic Programming:
Implementation Issues
17:00	
Flavio Cruz, Ricardo Rocha and Seth Goldstein
A Parallel Virtual Machine for Executing Forward-Chaining
Linear Logic Programs


FLoC Affiliations:

Due to the strong overlap between the CICLOPS-WLPE community
and several FLoC communities (in particular logic
(programming), verification, automated reasoning, rewriting
techniques, and SAT solving), the workshop is affiliated to
several conferences:
* 30th International Conference on Logic Programming (ICLP)
* 26th International Conference on Computer Aided
   Verification (CAV)
* 7th International Joint Conference on Automated Reasoning
   (IJCAR)
* Joint meeting of the 23rd EACSL Annual Conference on
   Computer Science Logic (CSL) and the 9th ACM/IEEE
   Symposium on Logic in Computer Science (LICS)
* 25th International Conference on Rewriting Techniques and
   Applications (RTA) joined with the 12th International
   Conference on Typed Lambda Calculi and Applications (TLCA)
* 17th International Conference on Theory and Applications
   of Satisfiability Testing (SAT)

In 2014, CICLOPS-WLPE also joins its program with the 11th
International Workshop on Constraint Handling Rules (CHR)
and has one joint session together with the Workshop on
Probabilistic Logic Programming (PLP).


Contact:

Thomas Stroeder <stroeder at informatik.rwth-aachen.de>
Terrance Swift <tswift at cs.stonybrook.edu>

-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241


More information about the Termtools mailing list