HOR  2007

4th International Workshop on Higher-Order Rewriting

Monday June 25, 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 technique frequently used for showing foundational properties of languages based on typed lambda-calculi. Historically, these proofs have been difficult to formalize in Twelf, in part because logical relations are difficult to define judgementally.
In this talk I discuss how we did it, and what lessons we have learned about the relationship between logical frameworks, the consistency of logical systems, 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, 2004).
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
  • 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.
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.

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:
  1. Using "traditional CRS" [1].
  2. Use of CRSX in the Virtual XML Query compiler [2]
Everything is done with general normalization using CRS rewrite rules.
[1] http://crsx.sourceforge.net/crsx-howto.pdf
[2] http://www.alphaworks.ibm.com/tech/virtualxml