RTA on Sunday, August 13th

Invited Talk (09:00‑10:00)
Chair: Ashish Tiwari
Location: Willow A/B

09:00‑10:00

Javier Esparza (Institute for Formal Methods in Computer Science, University of Stuttgart) Rewriting Models of Control-Flow [pdf] One of the problems faced by Software Model Checking is the complexity of control-flow mechanisms of modern programming languages. The combination of recursion and thread creation makes languages Turing-powerful even in the absence of data. For instance, the reachability of a program point is already undecidable for programs without variables! In this talk I will show that term rewriting can be used to model control-flow mechanisms in an elegant way, and to investigate the decidability and complexity of different combinations of mechanisms. In this approach term rewriting is studied from a different angle. The classical questions of termination and confluence are replaced by the reachability problem: given two terms t and t', can t be rewritten into t'? I will survey a number of results in this area.

Break (10:00‑10:30)

Session 4: Lambda Calculus (10:30‑12:30)
Chair: Delia Kesner
Location: Willow A/B

10:30‑11:00	Sylvain Salvati (National Institute of Informatics) Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear Lambda-Calculus We introduce syntactic descriptions, an extended type system for the linear $\lambda$-calculus. With this type system checking that a linear $\lambda$-term normalizes to another one reduces to type-checking. As a consequence this type system can be seen as a formal tool to design matching algorithms. In that respect, solving matching equations becomes a combination of type inference and proof search. We present such an algorithm for linear matching equations.In the case of second order equations, this algorithm stresses the similarities between linear matching in the linear $\lambda$-calculus and linear context matching. It uses tabular techniques and is a practical alternative to Huet's algorithm for these particular equations.
11:00‑11:30	Yo Ohta Masahito Hasegawa (RIMS, Kyoto University) A Terminating and Confluent Linear Lambda Calculus We present a rewriting system for the linear lambda calculus corresponding to the {!,-o}-fragment of intuitionistic linear logic. This rewriting system is shown to be strongly normalizing, and Church-Rosser modulo the trivial commuting conversion. Thus it provides a simple decision method for the equational theory of the linear lambda calculus. As an application we prove the strong normalization of the simply typed computational lambda calculus by giving a reduction-preserving translation into the linear lambda calculus.
11:30‑12:00	Ariel Arbiser (Universidad de Buenos Aires) Alexandre Miquel (PPS, Université Paris 7) Alejandro Ríos (Universidad de Buenos Aires) A Lambda-Calculus with Constructors We present an extension of the lambda(eta)-calculus with a case construct that propagates through functions like a head linear substitution, and show that this construction permits to recover the expressiveness of ML-style pattern matching. We then prove that this system enjoys the Church-Rosser property using a semi-automatic `divide and conquer' technique by which we determine all the pairs of commuting subsystems of the formalism (considering all the possible combinations of the nine primitive reduction rules). Finally, we prove a separation theorem similar to Böhm's theorem for the whole formalism.
12:00‑12:30	Jose Espirito Santo (Universidade do Minho) Maria João Frade (Universidade do Minho) Luís Pinto (Universidade do Minho) Structural Proof Theory as Rewriting The multiary version of the $\lambda$-calculus with generalized applications integrates smoothly both a fragment of sequent calculus and the system of natural deduction of von Plato. It is equipped with reduction rules (corresponding to cut-elimination/normalisation rules) and permutation rules, typical of sequent calculus and of natural deduction with generalised elimination rules. We argue that this system is a suitable tool for doing structural proof theory as rewriting. As an illustration, we investigate combinations of reduction and permutation rules and whether these combinations induce rewriting systems which are confluent and terminating. In some cases, the combination allows the simulation of non-terminating reduction sequences known from explicit substitution calculi. In other cases, we succeed in capturing interesting classes of derivations as the normal forms w.r.t to well-behaved combinations of rules. Among these are two classes, due to Herbelin and Mints, in bijection with normal, ordinary natural deductions. The relationship between these three classes is given a computational explanation, by the existence of three ways of expressing multiple application in the calculus.

Lunch break (12:30‑14:00)

Session 5: Theorem Proving (14:00‑15:30)
Chair: Jurgen Giesl
Location: Willow A/B

14:00‑14:30	Steven Obua (Technische Universität München) Checking Conservativity of Overloaded Definitions in Higher-Order Logic Overloading in the context of higher-order logic has been used for some time now. We define what we mean by Higher-Order Logic with Conservative Overloading (HOLCO). HOLCO captures how overloading is actually applied by the users of Isabelle. We show that checking whether definitions obey the rules of HOLCO is not even semi-decidable. The undecidability proof reveals strong ties between our problem and the dependency pair method by Arts and Giesl for proving termination of TRSs via the notion overloading TRS. The dependency graph of overloading TRSs can be computed exactly. We exploit this by providing an algorithm that checks the conservativity of definitions based on the dependency pair method and a simple form of linear polynomial interpretation; the algorithm also uses the strategy of Hirokawa and Middeldorp of recursively calculating the strongly connected components of the dependency graph. The algorithm is powerful enough to deal with all overloaded definitions that the author has encountered so far in practice. An implementation of this algorithm is available as part of a package that adds conservative overloading to Isabelle. This package also allows to delegate the conservativity check to external tools like the Tyrolean Termination Tool or the Automated Program Verification Environment.
14:30‑15:00	Adam Koprowski (Eindhoven University of Technology) Certified Higher-Order Recursive Path Ordering Recursive path ordering (RPO) is a well-known reduction ordering introduced by Dershowitz \cite{Der82}, that is useful for proving termination of term rewrite systems (TRSs). Jouannaud and Rubio generalized this ordering to the higher-order case thus creating the higher-order recursive path ordering (HORPO) \cite{JouRub99}. They proved that this ordering can be used for proving termination of higher-order TRSs which essentially comes down to proving well-foundedness of the union of HORPO and $\beta$-reduction relation of simply typed lambda calculus ($\lambda^{\rightarrow}$). This result entails well-foundedness of RPO and termination of $\lambda^{\rightarrow}$. This paper describes author's undertaking of providing a complete, axiom-free, fully constructive formalization of those results in the theorem prover Coq. Formalization is complete and hence it contains all the dependant results for $\lambda^{\rightarrow}$, multisets and multiset extension of the relation. Also decidability of HORPO has been proven and due to constructive nature of this proof a certified algorithm to verify whether two terms can be oriented with HORPO can be extracted from this proof. @inproceedings{JouRub99, author = {Jouannaud, J.-P. and Rubio, A.}, title = {The higher-order recursive path ordering}, pages = {402--411}, booktitle = {Proceedings of the 14th annual IEEE Symposium on Logic in Computer Science (LICS '99)}, year = {1999}, month = jul, address = {Trento, Italy} } @article{Der82, author = {Nachum Dershowitz}, title = {Orderings for Term-Rewriting Systems.}, journal = {Theor. Comput. Sci.}, volume = {17}, year = {1982}, pages = {279-301}, bibsource = {DBLP, http://dblp.uni-trier.de} }
15:00‑15:30	Takahito Aoto (RIEC, Tohoku University) Dealing with Non-Orientable Equations in Rewriting Induction Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.

Break (15:30‑16:00)

Session 6: System Descriptions (16:00‑17:00)
Chair: Eelco Visser
Location: Willow A/B

16:00‑16:15	Adam Koprowski (Eindhoven University of Technology) TPA: Termination Proved Automatically TPA is a tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion. The distinctive feature of TPA is the support for relative termination and the use of the technique of semantic labelling with natural numbers. Thanks to the latter TPA is capable of delivering automated termination proofs for some difficult TRSs for which all other tools fail.
16:15‑16:30	Yuki Chiba (RIEC, Tohoku University) Takahito Aoto (RIEC, Tohoku University) RAPT: A Program Transformation System based on Term Rewriting Chiba et al. (2005) proposed a framework of program transformation by template and automated verification of its correctness based on term rewriting. We describe RAPT (Rewriting-based Automated Program Transformation system) which implements this framework.
16:30‑16:45	Mathieu Turuani (Loria-Inria) The CL-Atse Protocol Analyser This paper presents an overview of the CL-Atse tool, an efficient and versatile automatic analyser for the security of cryptographic protocol. CL-Atse takes as input a protocol specified as a set of rewriting rules (IF format, produced by the AVISPA compiler), and uses rewriting and constraint solving techniques to model all reachable states of the participants and decide if an attack exists w.r.t. the Dolev-Yao intruder. Any state-based security property can be modelled (like secrecy, authentication, fairness, etc...), and the algebraic properties of operators like xor or exponentiation are taken into account with much less limitations than other tools, thanks to a complete modular unification algorithm. Also, useful constraints like typing, inequalities, or shared sets of knowledge (with set operations like removes, negative tests, etc...) can also be analysed.
16:45‑17:00	Ian Wehrman (Washington University in St. Louis) Aaron Stump (Washington University in St. Louis) Edwin Westbrook (Washington University in St. Louis) Slothrop: Knuth-Bendix Completion with a Modern Termination Checker A Knuth-Bendix completion procedure is parametrized by a reduction ordering used to ensure termination of intermediate and resulting rewriting systems. While in principle any reduction ordering can be used, modern completion tools typically implement only Knuth-Bendix and path orderings. Consequently, the theories for which completion can possibly yield a decision procedure are limited to those that can be oriented with a single path order. In this paper, we present a variant on the Knuth-Bendix completion procedure in which no ordering is assumed. Instead we rely on a modern termination checker to verify termination of rewriting systems. The new method is correct if it terminates; the resulting rewrite system is convergent and equivalent to the input theory. Completions are also not just ground-convergent, but fully convergent. We present an implementation of the new procedure, Slothrop, which automatically obtains such completions for theories that do not admit path orderings.

LICS-SAT-RTA Joint Banquet (19:00‑22:00)
Location: Grand Ballroom B