10 citations · 14 across the 5 of their papers we have counts for
5 papers
On Causal Equivalence by Tracing in String Rewriting
Vincent van Oostrom
We introduce proof terms for string rewrite systems and, using these, show that various notions of equivalence on reductions known from the literature can be viewed as different pe…
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the -calculus in Nominal Isabelle
Julian Nagele, Vincent van Oostrom, Christian Sternagel
We present a short proof of the Church-Rosser property for the lambda-calculus enjoying two distinguishing features: Firstly, it employs the Z-property, resulting in a short and el…
Nested Term Graphs (Work In Progress)
Clemens Grabmayer, Vincent van Oostrom
We report on work in progress on 'nested term graphs' for formalizing higher-order terms (e.g. finite or infinite lambda-terms), including those expressing recursion (e.g. terms in…
Layer Systems for Proving Confluence
Bertram Felgenhauer, Aart Middeldorp, Harald Zankl +1
We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers.…
Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples
Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks +2
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show…