The coordinates of the next TeReSe, an afternoon with presentations on rewriting, are as follows:

Wednesday November 14, 2012
13.15 - 17.30

Faculty of Sciences, Vrije Universiteit
De Boelelaan 1081, 1081 HV Amsterdam
room S631
how to get there and another how to get there.
VU campus map (pdf)

Programme

Afterwards there will be the opportunity to eat out together in the Korean restaurant Mika, Buitenveldertselaan 158a, 020 6614077.

Abstracts of the talks

Symbolic Evaluation Graphs and Term Rewriting
A General Methodology for Analyzing Logic Programs
by Jürgen Giesl (RWTH Aachen, Germany)
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). In this paper, 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.
Paper in PPDP 2012.

The dynamic pattern calculus as a higher-order pattern rewriting system
by Vincent van Oostrom (Utrecht University)
We show that Jay and Kesner's dynamic pattern calculus can be embedded into a higher-order pattern rewriting systems in the sense of Nipkow. Metatheoretical results, such as confluence and standardisation, are shown to obtain for the dynamic pattern calculus as a consequence of this embedding. The embedding also opens a way to study the semantics of Jay's programming language bondi based on pattern matching.

CRSX: Liberating HOAS from Strategy!
by Kris Rose (IBM research New York)
We recast CRSX (Combinatory Reduction Systems, eXtended) as a pure declarative approach yet practical executable specification language for compilers based on HOAS (Higher Order Abstract Syntax). We show how CRSX generalizes traditional parser generators to HOAS intermediate representations, and supports general strategy-free higher order rewriting on the intermediate HOAS representations to permit a concise declarative coding of full compilers from parsing to code generation. We specifically show how CRSX allows for the HOAS notation to be fully customizable so compiler projects can be based directly on existing specifications by working with the formal notations for all phases of the project yet still generate competitive C or Java code mechanically directly from the high level source. We argue that these attributes create an environment where we can effectively generate production compilers directly from readable formal specifications, and in IBM we are building a production compiler for W3C XQuery using CRSX. We show how elements of all phases from abstract syntax tree construction through code generation can be specified and implemented in CRSX, and comment on why we believe that the higher order rewriting approach of CRSX stands a real chance of succeeding in a wider sense than previous holistic compiler specification formalisms.

A Concurrent Persistent Functional Language
by Lesley Wevers (University of Twente)
In this talk I discuss the implementation of a persistent functional language with support for transactions. The state of the system consists of a set of bindings that map names to expressions. Transactions can evaluate an expression in the context of the current state, as well as update, create and delete bindings. Our implementation allows transactions to be executed concurrently by lazily evaluating the states that are produced by transactions, where concurrency control is provided by data-dependency between transactions. Our implementation uses a graph reducer based on template instantiation which has been modified to support the dynamic creation and removal of bindings. Additionally, we have developed a load balancing method for graph reduction based on sharing results between reduction threads, and randomising their reduction order. Our load balancing method allows parallel execution of transactions in such as way as to minimize the latency of individual transactions, as opposed to maximising the throughput of transactions as is common in work-stealing approaches to scheduling.

Finding small counter examples for term rewriting properties
by Hans Zantema (Eindhoven University of Technology)
Abstract: In the last TERESE we showed how by means of SAT solving small finite ARSs with a given list of rewriting properties can be found automatically. Here we extend this approach to simple TRSs rather than finite ARSs. For instance, no finite ARS exists that is locally confluent but not confluent and for which the reverse is terminating. However, a TRS having this combination of properties exists, for instance

1 → 2
1 → f(1)
2 → f(3)
3 → f(2)