Workshop PARIS - INNSBRUCK
Paris, September 15-16 2009
175, rue Chevaleret, Paris
Metro Chevaleret, line 6
Workshop of the PHC Amadeus project "Outils logiques d'analyse des programmes"
Programme
Tuesday, September 15
Wednesday, september 16
Abstracts:
Elaine Pimentel: A formal framework for specifying sequent calculus proof systems (Joint work with Dale Miller).
Abstract: Intuitionistic logic and intuitionistic type systems are
commonly used as frameworks for the specification of natural deduction
proof systems. In this paper we combine classical linear logic and a
simple scheme for induction to build the Llinda logic and show that
Llinda can be used as a logical framework to specify sequent calculus
proof systems and to establish some simple consequences of encoded
sequent calculus proof systems. In particular, derivability of the
sets of rules of one proof system from another can be decided by a
simple procedure that is implemented via bounded logic
programming-style search. We also show that initial rules can be
restricted to atoms and that cuts can be eliminated for any
object-logic whose Llinda specifications satisfy simple and decidable
conditions called homogeneous and coherence. To further illustrate the
strengths of this framework, we extend the definition of coherence and
provide a new, semi-automated proof of cut-elimination for Girard's
Logic of Unity (LU). We also study aspects of invertibility of rules
and the use of sub-exponentials in order to deal with several
substructural logics..
Aart Middeldorp: Decreasing Diagrams and Relative Termination
Abstract: In this talk, based on joint work with Nao Hirokawa, we present a new
confluence result for left-linear term rewrite systems based on critical
pairs and relative termination. The proof is based on the decreasing
diagrams technique. We further show how to encode the rule-labeling
heuristic for decreasing diagrams as a satisfiability problem. We give
experimental data for both methods.
Delia Kesner: Pattern Calculi
Abstract: Modern functional programming and theorem provers make use of static
terms - known as patterns - to filter relevant structure of data.
This standard model can be generalised by promoting patterns to
first-class citizens so that they become dynamic: they can be passed
as parameters, evaluated and returned as results. Two new forms of
polymorphism, called path and pattern polymorphism, can now be
expressed.
In this talk we describe a unique general framework, parametrised by a
pattern-matching algorithm, which is able to specify static as well as
dynamic pattern calculi. Expressive power and confluence of such
languages are discussed.
Georg Moser: Complexity of Term Rewrite Systems
Abstract: In order to assess the complexity of a (terminating) TRS it is natural
to look at the maximal length of derivations. Roughly such an analysis
is conceivable as a worst-case complexity analysis of the functions
computed by the given TRS. In the talk we will review recent results
in this area. In particular results on automatable techniques that
verify that the given TRS admits atmost polynomial (in the size of the
start term) lengths of derivations will be discussed.
Thibaut Balabonski: Optimality in the Weak Pure Pattern Calculus
Abstract: Pattern matching is usually seen as an extension of the core theory of functional programming. It is thus out of the scope of most theoretical works on efficient evaluation or optimality, since those are restricted to lambda-calculus.
This talk is about efficiency and sharing of computation in the Pure Pattern Calculus, a framework which integrates pattern matching as a base mechanism.
We will see how an analysis of the calculus can lead to the description of an interesting implementation. Indeed, we will have a formal account of its efficiency by proving it optimal with respect to some given restrictions.
Andreas Schnabl: The derivational complexity induced by the dependency pair method
Abstract: In this talk, we first give an introduction into polynomial interpretations, and
the dependency
pair method, two important methods in automatic termination proving.
Then we discuss the upper bounds on the derivational complexity induced
by such termination proofs:
It is well-known that polynomial interpretations give a double exponential upper
bound, which can be improved if the polynomials are suitably restricted.
On the other hand, the derivational complexity induced by the (basic) dependency
pair method based on some termination proof method is triple exponential in
the upper bound induced by that method when used directly.
Sarah Winkler: Automatic Termination Tools in Knuth-Bendix Completion
Abstract: Knuth-Bendix completion, a standard calculus in automated reasoning, is traditionally
parameterized by a reduction order, which is a highly critical factor for the success of
a derivation. Different approaches were proposed to tackle this problem. Among them
are (1) the inference system for completion with multiple reduction orderings
introduced by Kurihara and Kondo (1999) and (2) the inference system for completion
with external termination provers proposed by Wehrman, Stump and Westbrook
(2006). In this talk the MKBtt method is outlined, which combines these two
approaches. The respective implementation proves to be a comparatively fast and
powerful automatic completion tool.
Martin Avanzini: Syntactic Implicit Computational Complexity Analysis
Abstract: Proving termination of a rewrite system is a major research field in
rewriting, and consequently powerful techniques to (automatically)
verify termination have been introduced over the last decades. From a
proof of termination, we can often infer vital information about the
length of derivations admitted by a TRS, that is, such termination
techniques can in principle also be employed for a complexity analysis.
However, in order to extract interesting complexity certificates, the
employed termination technique often needs to be suitable tamed.
In this talk we show ideas from implicit complexity theory can be
employed for that purpose. In particular, I will introduce polynomial
path orders (POP*), a restriction of the well known multiset path order.
A proof of termination by means of POP* certifies, besides termination,
that the length of derivations is bounded by a polynomial in the size of
the start term. In turn, such a bound can then be used to also reason
about the implicit complexity of the function computed by the given
TRSs. In particular, I will present simple syntactic criteria that
guarantee that the computed function belongs to the class of polytime
computable functions.
Fabien Renaud: The Prismoid of Resources.
Abstract: We define a framework called the prismoid of resources where each vertex is a lambda calculus with the possibility of having different explicit resources and/or explicit cut elimination based on a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, substitution operations. For all the calculi in the prismoid we show simulation of beta reduction, confluence, preservation of beta-strong normalisation and strong normalisation for typed terms. Full composition also holds for the prismoid base handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs..
Séverine Maingaud: