4th International Workshop on Higher-Order Rewriting
2007 Paris, France
- Carsten Schürmann: On the formalization of logical relation arguments in Twelf
- Tait's method (a.k.a. proof by logical relations) is a powerful proof
frequently used for showing foundational properties of languages based
lambda-calculi. Historically, these proofs have been difficult to
Twelf, in part because logical relations are difficult to define
In this talk I discuss how we did it, and what lessons we have learned
relationship between logical frameworks, the consistency of logical
well-founded orderings, and proof theory.
This is joint work with Jeffrey Sarnat.
- Tarmo Uustalu: Circular proofs = Mendler in sequent form
- I present an interesting application of higher-order typed equational
reasoning to structural proof theory. First I describe a simply typed
lambda-calculus with inductive and coinductive types and guarded
(co)recursion in the style of N. P. Mendler. This is a higher-order
natural deduction system. Guardedness is expressed with type
polymorphism. Then I show that remoulding this system as a
higher-order sequent calculus yields a reconstruction with a solid
foundation of Cockett and Santocanale's calculus of circular proofs
(cf. Dam and Sprenger, Brotherston and Simpson).
- Andreas Abel: Syntactical strong normalization for intersection types with term rewriting rules
- We investigate the intersection type system of Coquand and Spiwack
with rewrite rules and natural numbers and give an elementary proof
of strong normalization which can be formalized in a weak metatheory.
- Lisa Allali: Algorithmic equality in Heyting arithmetic modulo
- In this paper we propose a new presentation of Heyting arithmetic modulo where axioms are replaced by rewrite rules. We focus on the definition of equality in this theory, especially on the fact that Leibniz's property is a consequence rather than the essence of this definition.
- Takahito Aoto and Toshiyuki Yamada: Argument filterings and usable rules for simply typed dependency pairs
- Simply typed term rewriting proposed by Yamada (RTA, 2001) is a framework
of higher-order term rewriting without bound variables. The dependency pair
framework for simply typed term rewriting (RTA, 2005) has been proposed by
extending the first-order dependency pair method introduced by Arts and Giesl
(TCS, 2000) and subterm criterion introduced by Hirokawa and Middeldorp (RTA,
In this paper, we incorporate into the simply typed dependency pair framework termination criteria using reduction pairs and related refinements. In particular, we extend the notions of argument filterings (Arts and Giesl, 2000) and usable rules (Hirokawa & Middeldorp 2004, Thiemann et. al. 2004) of first-order dependency pairs, for the simply typed dependency pairs.
- Lionel Marie-Magdeleine and Serguei
Soloviev: Non-standard reductions in simply-typed, higher order and dependently-typed systems
- Earlier we studied some possibilities to add non-standard
reductions to typed lambda-calculus with inductive types
in such a way that SN and CR properties would be preserved.
The aim was to open new possibilities for direct incorporation
of computational algorithms in Proof Assistants.
Some new methods to prove SN and CR were developped.
In this talk we discuss their generalization to higher order and
dependent type system cases.
- Kristoffer Rose: CRSX - an open source platform for experiments with higher-order rewriting
- The SourceForge CRSX project aims at implementing a generic higher order rewrite engine based on Klop's Combinatory Reduction Systems (CRS) formalism. The specific goals of the CRSX project are to
This paper summarizes how the current prototype implementation in Java (an open source platform) partially achieves these goals: the CRS abstraction that is actually implemented, the Java interfaces allowing using the engine on "foreign" terms, and how some extensions are enabled (and some not yet). We give examples from our ongoing work on an optimizing compiler for the W3C XQuery language.
- provide a generic higher order rewrite engine that
- is easy to embed in other projects such as compiler optimizers,
- is simple to extend with experimental features, and
- runs on a universally available open source platform.
- Max Schäfer: Elements of a categorical semantics for the Open Calculus of Constructions
- The Open Calculus of Constructions, introduced by Stehr in his 2001 thesis, is a type theory in the style of the Calculus of Constructions incorporating concepts from Rewriting Logic. We describe a categorical semantics for a subsystem of OCC, which is obtained by enriching a D-category based semantics with a 2-category structure. The resulting semantics is sound and conceivably encompasses a wide variety of different models for the calculus; thus it could serve as a basis for further meta-theoretical investigations of OCC and perhaps also related systems.
- Daniel Ventura, Mauricio Ayala-Rincon and Fairouz
Kamareddine: Principal typings for explicit substitutions calculi
- Having principal typings (for short PT) is an important property of type
systems. This property guarantees the possibility of type deduction which means
it is possible to develop a complete and terminating type inference mechanism.
It is well-known that the simply typed lambda-calculus has this property, but
recently, J. Wells has introduced a system-independent definition of PT which
allows to prove that some type systems do not satisfy PT. The main
computational drawback of the lambda-calculus is the implicitness of the notion
of substitution, a problem which in the last years gave rise to a number of
extensions of the lambda-calculus where the operation of substitution is
treated explicitly. Unfortunately, some of these extensions do not necessarily
preserve basic properties of the simply typed lambda-calculus such as
preservation of strong normalization. We consider two systems of explicit
substitutions (lambda-sigma and lambda s_e) and we show that they can be
accommodated with an adequate notion of PT.
Specifically, our results can be summarized as follows:
- We introduce PT notions for the simply typed versions of the lambda-sigma and the lambda s_e-calculus according to Wells' system-independent notion of PT.
We show that these versions of the lambda-sigma and the lambda s_e satisfy PT by revisiting previously introduced type inference algorithms.
- Kristoffer Rose: Demonstration of CRSX
I'll demonstrate the capabilities of the CRSX engine:
Everything is done with general normalization using CRS rewrite rules.
- Using "traditional CRS" .
- Use of CRSX in the Virtual XML Query compiler