
List of accepted papers
Invited lectures
 Detecting bugs in Erlang programs using static analysis
 Konstantinos Sagonas
This talk will review the main techniques used in the Dialyzer
(Discrepancy AnaLYZer of ERlang programs) defect detection tool.
Dialyzer employs various forms of static program analysis to
automatically identify software errors in large applications
written in
Erlang, a concurrent functional language developed by Ericsson and
commonly used for developing telecommunications software. Dialyzer is
completely automatic, relatively fast, requires no annotations from its
user to detect defects, and is exceptional in that it does not report
any false positives.
The heart of Dialyzer's analysis is intermodular
inference of success typings for Erlang functions and the talk will
explain what success typings are and how they differ from type inference
in statically typed languages.
alyzer, which nowadays is part of the Erlang/OTP (Open Telecom
Platform) system, has been applied to large code bases of Erlang code
and has identified a significant number of software defects that have
remained unnoticed after years of extensive testing. The talk will also
describe experiences and main lessons learned from Dialyzer's
development and from feedback from its user community.
More information about the tool and a set of related publications can be
found in
Dialyzer's website.
 Local Reasoning About Storable Locks
 Josh Berdine
This talk will present a resourceoriented program logic that is able to
reason about concurrent heapmanipulating programs with unbounded
numbers of dynamicallyallocated locks, and note an extension to
storable threads. The logic is inspired by concurrent separation logic,
but handles these more realistic concurrency primitives. We demonstrate
that the proposed logic allows for local reasoning about programs that
exhibit a high degree of information hiding in their locking mechanisms.
Soundness is proved using a novel threadlocal fixedpoint semantics.

 Regular Directional Types for Logic Programs
 Witold Charatonik

Directional types assign each predicate in a logic program a pair of an input
and an output type describing the possible argument terms before and after a
call of the predicate. Regular types use tree automata for the effective
representation of recursive data structures such as lists. In this talk, we
discuss a type system for logic programs based on regular directional types.
Regular papers
 Formalizing and Verifying Semantic Type Soundness of a Simple Compiler
 Nick Benton and Uri Zarfaty

We describe a semantic type soundness result, formalized in the Coq proof
assistant, for a compiler from a simple imperative language with
heapallocated data into an idealized assembly language. Types in the
highlevel language are interpreted as binary relations, built using both
secondorder quantification and a form of separation structure, over stores
and code pointers in the lowlevel machine.
 Interactive, Scalable, Declarative Program Analysis: From Prototype to Implementation
 William C. Benton and Charles N. Fischer

Static analyses provide the semantic foundation for tools ranging from
optimizing compilers to refactoring browsers and advanced debuggers.
Unfortunately, developing new analysis specifications and implementations is
often difficult and errorprone. Since analysis specifications are generally
written in a declarative style, logic programming presents an attractive model
for producing executable specifications of analyses. However, prior work on
using logic programming for program analysis has focused exclusively on solving
constraints derived from program texts by an external preprocessor. In this
paper, we present DIMPLE, an analysis framework for Java bytecodes implemented
in the Yap Prolog system. DIMPLE provides both a representation of Java
bytecodes in a database of relations and a declarative domainspecific language
for specifying new analyses as queries over this database. DIMPLE thus enables
users to use logic programming for every step of the analysis development
process, from specification to prototype to implementation. We demonstrate
that our approach facilitates rapid prototyping of new program analyses and
produces executable analysis implementations that are speedcompetitive with
specialized analysis toolkits.
 Userdefinable Rule Priorities for CHR
 Leslie De Koninck, Tom Schrijvers and Bart Demoen

This paper introduces CHRrp: Constraint Handling Rules with userdefinable
rule priorities. CHRrp offers flexible execution control which is lacking in
CHR. A formal operational semantics for the extended language is given and is
shown to be an instance of the theoretical operational semantics of CHR. It is
discussed how the CHRrp semantics influences confluence results. A translation
scheme for CHRrp programs with static rule priorities into (regular) CHR is
presented. The translation is proven correct and benchmark results are given.
CHRrp is related to priority systems in other constraint programming and rule
based languages.
 Practical use of polynomials over the reals in proofs of termination
 Salvador Lucas

Nowadays, polynomial interpretations are an essential ingredient in the
development of tools for proving termination. Recently, we have proven that
polynomial interpretations over the reals are strictly better for proving
polynomial termination of rewriting than those which only use integer
coefficients. Some essential aspects of their practical use, though, remain
unexplored or underdeveloped. In this paper, we compare the two existing
frameworks for using polynomial intepretations over the reals and show that one
of them is strictly better than the other, thus making a suitable choice for
implementations. We also prove that the use of algebraic real coefficients in
the interpretations suffice for termination proofs. We also discuss the use of
algorithms and techniques from Tarski's firstorder logic of the real closed
fields for implementing their use in proofs of termination. We argue that more
standard constraintsolving techniques are better suited for this. We propose
an algorithm to solve the polynomial constraints which arise when specific
finite subsets of rational (or even algebraic real) numbers are considered for
giving value to the coefficients. We provide a preliminary experimental
evaluation of the algorithm which has been implemented as part of the
termination tool MUTERM.
 Type Safe Dynamic Linking for JVM Access Control
 Christian Skalka

The Java JDK security model provides an access control mechanism for the JVM
based on dynamic stack inspection. Previous results have shown how stack
inspection can be enforced at compile time via wholeprogram type analysis, but
features of the JVM present significant remaining technical challenges. For
instance, dynamic dispatch at the bytecode level requires special consideration
to ensure flexibility in typing. Even more problematic is dynamic class loading
and linking, which disallow a purely static analysis in principle, though the
intended applications of the JDK exploit these features. We propose an
extension to existing bytecode verification, that enforces stack inspection at
link time, without imposing new restrictions on the JVM class loading and
linking mechanism. Our solution is more flexible than existing type based
approaches, and establishes a formal type safety result for bytecodelevel
access control in the presence of dynamic class linking.
 Systematic Generation of GlassBox Test Cases for Functional Logic Programs
 Sebastian Fischer and Herbert Kuchen

We employ the narrowingbased execution mechanism of the functional logic
programming language Curry in order to automatically generate a system of test
cases for glassbox testing of Curry programs.
The test cases for a given function are computed by narrowing a call to that
function with initially uninstantiated arguments.
The generated test cases are produced w.r.t. a selected codecoverage criterion
such as controlflow coverage. Besides an adaption of the notion of
controlflow coverage to functional (logic) programming, we present a novel
coverage criterion for this programming paradigm. A particular difficulty of
the adaption is the handling of laziness.
 Mechanized Metatheory ModelChecking
 James Cheney and Alberto Momigliano

The problem of formalizing and proving metatheoretic properties of programming
language calculi, type systems, operational semantics, and related formal
systems has received considerable attention recently. However, the dual problem
ofsearching for errors in such formalizations has received comparatively little
attention. In this paper, we consider the problem of bounded modelchecking
for metatheoretic properties of formal systems specified using nominal logic.
In contrast to current state of the art for metatheory verification, our
approach is fully automatic, does not require expertise in theorem proving on
the part of the user, and produces counterexamples in the common case that a
flaw is detected. Two counterexample search strategies are considered, one
employing negationasfailure and the other based on negation elimination; we
compare the two approaches from the point of view of semantic complexity,
implementation overhead, and efficiency.
 Relational Semantics for EffectBased Program Transformations with Dynamic Allocation
 Nick Benton, Andrew Kennedy, Lennart Beringer and Martin Hofmann

We give a denotational semantics to a regionbased effect systemtracking
reading, writing and allocation in a higherorder language with dynamically
allocated integer references.
Effects are interpreted in terms of the preservation of certain binary
relations on the store, parameterized by regionindexed partial bijections on
locations.
The semantics validates a number of effectdependent program equivalences and
can thus serve as a foundation for effectbased compiler transformations.
 HigherOrder Semantic Labelling for Inductive Datatype Systems
 Makoto Hamana

We give a novel transformation for proving termination of higherorder rewrite
systems in the format of Inductive Data Type Systems (IDTSs) by Blanqui,
Jouannaud and Okada. The transformation called higherorder semantic labelling
attaches algebraic semantics of the arguments to each function symbol. We
systematically define the labelling and show that labelled systems give
termination models in the framework of Fiore, Plotkin and Turi's binding
algebras. As applications, we give simple proofs of termination of the explicit
substitution system lambdaX and currying transformation via higherorder
semantic labelling. Moreover, we prove new results of modularity of termination
of IDTSs by introducing the notion of solid IDTSs. We prove termination is
preserved under the disjoint union of:
 an IDTS and a higherorder program scheme (HORPS),
 βreduction, a confluent firstorder system and a HORPS,
 an IDTS and βreduction.
 Debugging Parallel Functional Languages
 Alberto de la Encina, Luis Llana, Fernando Rubio and Mercedes HidalgoHerrero

Due to the use of higherorder functions and laziness, debugging lazy
functional programs is not a trivial task. Fortunately, several debuggers have
appeared during the last years. However, the difficulty of the debugging
process is increased when considering parallel extensions of lazy functional
languages. Thus, it is necessary not only to develop practical debuggers, but
also to provide a clear semantic environment to understand what the debuggers
should do. In this paper we present a formal framework for debugging two
different parallel extensions of the lazy functional language Haskell. In
order to do that, we define an operational semantics model which allows us to
deal with sideeffects and parallelism. By doing so, we provide a formalization
of a parallel debugger we have already implemented by extending the sequential
debugger Hood.
 Computing with Subspaces
 Bernd Brassel and Sergio Antoy

We propose a new definition and use of a primitive, called getAllValues, for
computing all the values of a nondeterministic expression in a functional
logic program. Our proposal restricts the validity of the argument of
getAllValues. This restriction ensures that essential language features, such
as the calltime choice semantics, the independence of the order of evaluation,
and the referential transparency of the language, are preserved when
getAllValues is executed. Up to now, conflicts between these language features
and primitives like getAllValues have been seen as one of the main problems for
employing such primitives in functional logic languages.
 RealTime Rewriting Semantics of Orc
 Musab AlTurki and José Meseguer

Orc is a language proposed by Jayadev Misra for orchestration of
distributed services. Orc is very simple and elegant, based on a few basic
constructs, and allows succinct and understandable programming of sophisticated
applications. However, because of its realtime nature and the different
priorities given to internal and external events in an Orc program, giving a
formal operational semantics that captures the realtime behavior of Orc
programs is nontrivial and poses some interesting challenges. In this paper we
propose such a realtime operational Orc semantics, that captures the informal
operational semantics given by Misra. This operational semantics is given as a
rewrite theory in which the elapse of time is explicitly modeled. The
priorities between internal and external events are also modeled in two
alternative ways: (i) by a rewrite strategy; and (ii) by adding extra
conditions to the semantic rules. Since rewriting logic has efficient
implementations such as Maude, we also get, directly out of the semantic
definitions, both an Orc interpreter and an LTL model checker for Orc programs.
 A Larger Decidable Semiunification Problem
 Brad Lushman and Gordon V. Cormack

We present a graphtheoretic framework in which to study instances of the
semiunification problem (SUP), which is known to be undecidable, but has
several known and important decidable subsets. One such subset, the _acyclic_
semiunification problem (ASUP), has proved useful in the study of polymorphic
type inference. We present graphtheoretic criteria in our framework that
exactly characterize the ASUP acyclicity constraint. We then use our framework
to find a decidable subset of SUP (which we call RASUP), which has a more
natural description than ASUP, and strictly contains it.
 Putting Declarative Programming into the Web: Translating Curry to JavaScript
 Michael Hanus

We propose a framework to construct weboriented user interfaces in a
highlevel way by exploiting declarative programming techniques. Such user
interfaces are intended to manipulate complex data in a typesafe way, i.e., it
is ensured that only typecorrect data is accepted by the interface, where
types can be specified by standard types of a programming language as well as
any computable predicate on the data. The interfaces are webbased, i.e., the
data can be manipulated with standard web browsers without any specific
requirements on the client side. However, if the client's browser has
JavaScript enabled, one could also check the correctness of the data on the
client side providing immediate feedback to the user and reducing network
traffic. In order to release the application programmer from the tedious
details to interact with JavaScript, we propose an approach where the
programmer must only provide a declarative description of the requirements of
the user interface from which the necessary JavaScript programs and HTML forms
are automatically generated. This approach leads to a very concise and
maintainable implementation of webbased user interfaces. We demonstrate an
implementation of this concept in the declarative multiparadigm language Curry
where the integrated functional and logic features are exploited to enable the
high level of abstraction proposed in this paper.
 Induction for Positive Almost Sure Termination
 Isabelle Gnaedig

In this paper, we propose an inductive approach to prove positive almost sure
termination of probabilistic rewriting under the innermost strategy. We extend
to the probabilistic case a technique we proposed for termination of usual
rewriting under strategies. The induction principle consists in assuming that
terms smaller than the starting terms for an induction ordering are positively
almost surely terminating. The proof is developed in generating proof trees,
modelizing rewriting trees, in alternatively applying abstraction steps,
expressing the application of the induction hypothesis, and narrowing steps,
simulating the possible rewriting steps after abstraction. This technique is
fully automatable for rewrite systems on constants, very useful to modelize
probabilistic protocols.
 Unfolding in CHR
 Paolo Tacchella, Maria Chiara Meo and Maurizio Gabbrielli

Program transformation is an appealing technique which allows to improve
runtime efficiency, spaceconsumption and more generally to optimize a given
program. Essentially it consists of a sequence of syntactic program
manipulations which preserves some kind of semantic equivalence. One of the
basic operations which is used by most program transformation systems is
unfolding which consists in the replacement of a procedure call by its
definition. While there is a large body of literature on transformation and
unfolding of sequential programs, very few papers have addressed this issue for
concurrent languages and, to the best of our knowledge, no one has considered
unfolding of CHR programs.
This paper is a first attempt to define a correct unfolding system for CHR
programs. We define an unfolding rule, show its correctness and discuss some
conditions which can be used to delete an unfolded rule while preserving the
program meaning.
 Nonmonotonic Inductive Logic Programming by Instance Patterns
 Chongbing Liu and Enrico Pontelli

In this paper, we present a new approach, called NMILPIP, for inductive
learning in the context of nonmonotonic logic frameworks.This approach is based
on the notations of concept instances and instance patterns.When a strictly
correct Horn theory cannot be induced, this approach induces a normal logic
program, by specializing a previously learned overlygeneral theory. The
advantages of this approach over others include:
 it does not rely on existing ILP systems, and it avoids
many of the effectiveness and efficiency drawbacks of
ordinary ILP systems;
 no theorem prover is needed during the learning process;
 it introduces negation as failure (NAF) of existing predicates
and introduces new abnormality predicates only when necessary,
making the final theory more compact.
 A simple rewrite notion for calltime choice semantics
 Francisco LopezFraguas, Juan RodriguezHortala and Jaime SanchezHernandez

Nonconfluent and nonterminating rewrite systems are interesting from the
point of view of programming. In particular, existing functional logic
languages use such kind of rewrite systems to define possibly nonstrict
nondeterministic functions. The semantics adopted for nondeterminism is
calltime choice, whose combination with nonstrictness is not a trivial issue
that has been addressed from a semantic point of view in the Constructorbased
Rewriting Logic (CRWL) framework. We investigate here how to express calltime
choice and nonstrict semantics from a point of view closer to classical
rewriting. The proposed notion of rewriting uses an explicit representation for
sharing with letconstructions and is proved to be equivalent to the CRWL
approach.
 Efficient Trust Management Policy Analysis from Rules
 Katia Hristova, K. Tuncay Tekle and Yanhong A. Liu

This paper describes a systematic method for deriving efficient algorithms and
precise time complexities from extended Datalog rules as it is applied to the
analysis of trust management policies specified in SPKI/SDSI, a wellknown
trust management framework designed to facilitate the development of secure and
scalable distributed computing systems. The approach of expressing policy
analysis problems as extended Datalog rules is much simpler than previous
techniques for analysis of SPKI/SDSI policies. Our method also derives better,
more precise time complexities than before in addition to generating complete
algorithms and data structures. The method is general, with many applications
beyond policy analysis. It extends our previous method for Datalog to handle
list constructors, external functions, and queries.
 Feasible reactivity in a synchronous πcalculus
 Roberto Amadio and Frederic Dabrowski

Reactivity is an essential property of a synchronous program. Informally, it
guarantees that at each instant the program fed with an input will “react”
producing an output. In the present work, we consider a refined property that
we call feasible reactivity. Beyond reactivity, this property guarantees that
at each instant both the size of the program and its reaction time are bounded
by a polynomial in the size of the parameters at the beginning of the
computation and the size of the largest input. We propose a method to annotate
programs and we develop related static analysis techniques that guarantee
feasible reactivity for programs expressed in the Sπcalculus.
The latter is a synchronous version of the πcalculus based on the SL
synchronous programming model.

