Deduction using the ProofWeb system (2009)
Cezary Kaliszyk, Femke Van Raamsdonk, Freek Wiedijk, Maxim Hendriks, Roel De Vrijer
This is the manual of the ProofWeb system that was implemented at the Radboud University Nijmegen and the Free University Amsterdam in the SURF education innovation project Web deduction for...
Lambda Calculus with Patterns (2008)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
Abstract. In this paper we revisit the λ-calculus with patterns, originating from the practice of functional programming language design. We treat this feature in a framework ranging from pure...
Vrije Universiteit Amsterdam BARENDREGT’S LEMMA (2008)
Abstract. Barendregt’s Lemma in its original form is a statement on Combinatory Logic that holds also for the lambda calculus and gives important insight into the syntactic interplay between...
Iterative Path Orders 1 Iterative Path Orders Extended abstract (2008)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
In the first half of this paper we give an alternative version of the recursive path order (RPO) for first-order term rewriting, which is ‘iterative ’ rather than recursive. Hence the name...
Iterative Lexicographic Path Orders (2008)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
Abstract. We relate Kamin and Lévy’s original presentation of lexicographic path orders (LPO), using an inductive definition, to a presentation, which we will refer to as iterative lexicographic...
Descendants and Origins in Term Rewriting (2007)
Inge Bethke Jan, Jan Willem Klop, Roel De Vrijer
In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first order term rewriting and -calculus, their finitary...
A Geometric Proof of Confluence by Decreasing Diagrams (2007)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
Recently a new confluence criterion for confluence was found using decreasing diagrams, as a generalization of several wellknown confluence criteria in abstract rewriting such as the strong...
Software ENgineering Infinitary normalization (2005)
J. W. Klop, Jan Willem Klop, Roel De Vrijer
CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented structure and is grouped into four clusters. Listed below...
Infinitary Normalization (2005)
Jan Willem Klop, Roel De Vrijer
abstract. In infinitary orthogonal first-order term rewriting the properties confluence (CR), Uniqueness of Normal forms (UN), Parallel Moves Lemma (PML) have been generalized to their infinitary...
. DRAFT Iterative path orders (2004)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
In Dershowitz’s original presentation recursive path orders (RPO) are defined by means of recursion. In Bergstra and Klop’s presentation RPOs are operationally defined by means of a set of term...
Four Equivalent Equivalences of Reductions (2002)
Vincent Van Oostrom, Roel De Vrijer
Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a di#erent order. We present four characterisations of such a notion of...
A Calculus of Lambda Calculus Contexts (2001)
The calculus c serves as a general framework for representing contexts. Essential features are control over variable capturing and the freedom to manipulate contexts before or after hole lling, by a...
A geometric proof of confluence by decreasing diagrams (2000)
J. W. Klop, V. Van Oostrom, R. De Vrijer, Mathematisch Centrum (smc, The Dutch Foundation, Jan Willem Klop, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Extending partial combinatory algebras (1999)
We give a negative answer to the question whether every partial combinatory algebra can be completed. The explicit counterexample will be an intricately constructed term model, the construction and...
The context calculus λc (Extended Abstract) (1999)
Mirna Bognar Roel de Vrijer Abstract The calculus c serves as a general framework for representing contexts. Essential features are control over variable capturing and the freedom to manipulate...
Descendants and Origins in Term Rewriting (1999)
I. Bethke, Jan W. Klop, R. De Vrijer, Inge Bethke, Jan Willem Klop, Roel De Vrijer
In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first order term rewriting and -calculus, their finitary...
Completing Partial Combinatory Algebras with Unique Head-Normal Forms (1995)
I. Bethke, J. W. Klop, R. De Vrijer, Issn -x, Inge Bethke, Jan Willem Klop, ...
In this note, we prove that having unique head-normal forms is a sufficient condition on partial combinatory algebras to be completable. As application, we show that the pca of strongly normalizing...
Modularity of confluence: A simplified proof (1994)
Jan Willem Klop, Aart Middeldorp, Yoshihito Toyama, Roel De Vrijer
In this note we present a simple proof of a result of Toyama which states that the disjoint union of confluent term rewriting systems is confluent.