16 Search Results for "van Oostrom, Vincent"

Document
DOI: 10.4230/LIPIcs.CSL.2026.37
Towards the Type Safety of Pure Subtype Systems

Authors: Valentin Pasquale and Álvaro García-Pérez

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Hutchins' Pure Subtype Systems (PSS) offer a unified framework for types and terms, promising significant advancements in language design for features like dependent types and higher-order subtyping. However, the theory has been hampered by a critical gap: a proof of type safety has remained an open problem for over a decade. The original attempt to prove this property relied on the conjectured commutativity of two fundamental reduction relations, equivalence and subtyping. Proving transitivity elimination, however, requires this commutativity, a property that is notoriously difficult to establish for higher-order subtyping systems. In this paper, we address this issue by introducing Machine-Based PSS (MPSS), a novel reformulation of the original system. MPSS integrates a continuation stack mechanism, reminiscent of the Krivine Abstract Machine, to keep track of arguments that are passed during function application, enabling more fine-grained reductions. This architectural change exposes crucial intermediate reduction steps that were absent in the original PSS. The primary contribution of our work is a direct proof that the equivalence and subtyping reductions in MPSS commute. This result formally establishes transitivity elimination, which is the cornerstone of the inversion lemma required for type safety. We conclude by outlining a pathway from our foundational result to a complete, type-safe system, thereby paving the way for the practical realization of PSS-based languages.
Cite as

Valentin Pasquale and Álvaro García-Pérez. Towards the Type Safety of Pure Subtype Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{pasquale_et_al:LIPIcs.CSL.2026.37,
  author =	{Pasquale, Valentin and Garc{\'\i}a-P\'{e}rez, \'{A}lvaro},
  title =	{{Towards the Type Safety of Pure Subtype Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.37},
  URN =		{urn:nbn:de:0030-drops-254626},
  doi =		{10.4230/LIPIcs.CSL.2026.37},
  annote =	{Keywords: Lambda calculus, Pure subtype systems, Dependent types, Higher-order subtyping, Type safety}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.39
Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper)

Authors: Nadeem Abdul Hamid

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The concept of permutations is fundamental in computer science, and is useful for specifying and reasoning about a variety of data structures and algorithms. This paper presents the implementation of a fully automated tactic for proving complex permutation goals within the Rocq Prover (formerly, Coq proof assistant). Our approach leverages proof by reflection and an iterative deepening search procedure to establish permutation relations on arbitrary lists composed of concatenation operations. We detail the construction of mapping/substitution environments, a unification algorithm, and metaprogramming tactics to automate the proof process. The potential impact of the tactic for goals involving permutations is demonstrated by significant reduction in proof script length for an existing non-trivial development.
Cite as

Nadeem Abdul Hamid. Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 39:1-39:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{abdulhamid:LIPIcs.ITP.2025.39,
  author =	{Abdul Hamid, Nadeem},
  title =	{{Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{39:1--39:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.39},
  URN =		{urn:nbn:de:0030-drops-246378},
  doi =		{10.4230/LIPIcs.ITP.2025.39},
  annote =	{Keywords: permutations, reflection, tactics, Rocq, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.13
Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized

Authors: Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Barendregt’s book on the untyped λ-calculus refines the inconsistent view of β-divergence as representation of the undefined via the key concept of head reduction. In this paper, we put together recent revisitations of some key theorems laid out in Barendregt’s book, and we formalize them in the Abella proof assistant. Our work provides a compact and refreshed presentation of the core of the book. The formalization faithfully mimics pen-and-paper proofs. Two interesting aspects are the manipulation of contexts for the study of contextual equivalence and a formal alternative to the informal trick at work in Takahashi’s proof of the genericity lemma. As a by-product, we obtain an alternative definition of contextual equivalence that does not mention contexts.
Cite as

Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot_et_al:LIPIcs.ITP.2025.13,
  author =	{Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
  title =	{{Barendregt’s Theory of the \lambda-Calculus, Refreshed and Formalized}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.13},
  URN =		{urn:nbn:de:0030-drops-246114},
  doi =		{10.4230/LIPIcs.ITP.2025.13},
  annote =	{Keywords: lambda-calculus, head reduction, equational theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.25
Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality

Authors: Ievgen Ivanov

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We show that every confluent abstract rewriting system (ARS) of the cardinality that does not exceed the first uncountable cardinal belongs to the class DCR₃, i.e. the class of confluent ARS for which confluence can be proved with the the help of the decreasing diagrams method using the set of labels {0,1,2} ordered in such a way that 0<1<2 (in the general case, the decreasing diagrams method with two labels is not sufficient for proving confluence of such ARS). Under the Continuum Hypothesis this result implies that the decreasing diagrams method is sufficient for establishing confluence of ARS on many structures of interest to applied mathematics and various interdisciplinary fields (confluence of ARS on real numbers, continuous real functions, etc.). We provide a machine-checked formal proof of a formalized version of the main result in Isabelle proof assistant using HOL logic and the HOL-Cardinals theory. An extended version of this formalization is available in the Archive of Formal Proofs.
Cite as

Ievgen Ivanov. Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ivanov:LIPIcs.FSCD.2025.25,
  author =	{Ivanov, Ievgen},
  title =	{{Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.25},
  URN =		{urn:nbn:de:0030-drops-236404},
  doi =		{10.4230/LIPIcs.FSCD.2025.25},
  annote =	{Keywords: confluence, decreasing diagrams method, rewriting systems, reduction, formal methods, formal proofs, formal verification, non-discrete models, nondeterministic models, interval models}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.24
Quantitative Types for the Functional Machine Calculus

Authors: Willem Heijltjes

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The Functional Machine Calculus (FMC, Heijltjes 2022) extends the lambda-calculus with the computational effects of global mutable store, input/output, and probabilistic choice while maintaining confluent reduction and simply-typed strong normalization. Based in a simple call-by-name stack machine in the style of Krivine, the FMC models effects through additional argument stacks, and introduces sequential composition through a continuation stack to encode call-by-value behaviour, where simple types guarantee termination of the machine. The present paper provides a discipline of quantitative types, also known as non-idempotent intersection types, for the FMC, in two variants. In the weak variant, typeability coincides with termination of the stack machine and with spine normalization, while exactly measuring the transitions in machine evaluation. The strong variant characterizes strong normalization through a notion of perpetual evaluation, while giving an upper bound to the length of reductions. Through the encoding of effects, quantitative typeability coincides with termination for higher-order mutable store, input/output, and probabilistic choice.
Cite as

Willem Heijltjes. Quantitative Types for the Functional Machine Calculus. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{heijltjes:LIPIcs.FSCD.2025.24,
  author =	{Heijltjes, Willem},
  title =	{{Quantitative Types for the Functional Machine Calculus}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.24},
  URN =		{urn:nbn:de:0030-drops-236391},
  doi =		{10.4230/LIPIcs.FSCD.2025.24},
  annote =	{Keywords: lambda-calculus, computational effects, intersection types}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.13
Simulating Dependency Pairs by Semantic Labeling

Authors: Teppei Saito and Nao Hirokawa

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We show that termination proofs by a version of the dependency pair method can be simulated by semantic labeling plus multiset path orders. By incorporating a flattening technique into multiset path orders the simulation result can be extended to the dependency pair method for relative termination, introduced by Iborra et al. This result allows us to improve applicability of their dependency pair method.
Cite as

Teppei Saito and Nao Hirokawa. Simulating Dependency Pairs by Semantic Labeling. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{saito_et_al:LIPIcs.FSCD.2024.13,
  author =	{Saito, Teppei and Hirokawa, Nao},
  title =	{{Simulating Dependency Pairs by Semantic Labeling}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.13},
  URN =		{urn:nbn:de:0030-drops-203423},
  doi =		{10.4230/LIPIcs.FSCD.2024.13},
  annote =	{Keywords: Term rewriting, Relative termination, Semantic labeling, Dependency pairs}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.22
α-Avoidance

Authors: Samuel Frontull, Georg Moser, and Vincent van Oostrom

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
When substitutions and bindings interact, there is a risk of undesired side effects if the substitution is applied naïvely. The λ-calculus captures this phenomenon concretely, as β-reduction may require the renaming of bound variables to avoid variable capture. In this paper we introduce α-paths as an estimation for α-avoidance, roughly expressing that α-conversions are not required to prevent variable capture. These paths provide a novel method to analyse and predict the potential need for α in different calculi. In particular, we show how α-path characterises α-avoidance for several sub-calculi of the λ-calculus like (i) developments, (ii) affine/linear λ-calculi, (iii) the weak λ-calculus, (iv) μ-unfolding and (iv) finally the safe λ-calculus. Furthermore, we study the unavoidability of α-conversions in untyped and simply-typed λ-calculi and prove undecidability of the need of α-conversions for (leftmost-outermost reductions) in the untyped λ-calculus. To ease the work with α-paths, we have implemented the method and the tool is publicly available.
Cite as

Samuel Frontull, Georg Moser, and Vincent van Oostrom. α-Avoidance. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{frontull_et_al:LIPIcs.FSCD.2023.22,
  author =	{Frontull, Samuel and Moser, Georg and van Oostrom, Vincent},
  title =	{{\alpha-Avoidance}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{22:1--22:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.22},
  URN =		{urn:nbn:de:0030-drops-180068},
  doi =		{10.4230/LIPIcs.FSCD.2023.22},
  annote =	{Keywords: \lambda-calculus, variable capture, \alpha-conversion, developments, safe \lambda-calculus, undecidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.10
The Functional Machine Calculus II: Semantics

Authors: Chris Barrett, Willem Heijltjes, and Guy McCusker

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
Cite as

Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barrett_et_al:LIPIcs.CSL.2023.10,
  author =	{Barrett, Chris and Heijltjes, Willem and McCusker, Guy},
  title =	{{The Functional Machine Calculus II: Semantics}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.10},
  URN =		{urn:nbn:de:0030-drops-174716},
  doi =		{10.4230/LIPIcs.CSL.2023.10},
  annote =	{Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.28
Compositional Confluence Criteria

Authors: Kiraku Shintani and Nao Hirokawa

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. In addition to them, we prove that Toyama’s parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.
Cite as

Kiraku Shintani and Nao Hirokawa. Compositional Confluence Criteria. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{shintani_et_al:LIPIcs.FSCD.2022.28,
  author =	{Shintani, Kiraku and Hirokawa, Nao},
  title =	{{Compositional Confluence Criteria}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.28},
  URN =		{urn:nbn:de:0030-drops-163095},
  doi =		{10.4230/LIPIcs.FSCD.2022.28},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.24
Z; Syntax-Free Developments

Authors: Vincent van Oostrom

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We present the Z-property and instantiate it to various rewrite systems: associativity, positive braids, self-distributivity, the lambda-calculus, lambda-calculi with explicit substitutions, orthogonal TRSs, .... The Z-property is proven equivalent to Takahashi’s angle property by means of a syntax-free notion of development. We show that several classical consequences of having developments such as confluence, normalisation, and recurrence, can be regained in a syntax-free way, and investigate how the notion corresponds to the classical syntactic notion of development in term rewriting.
Cite as

Vincent van Oostrom. Z; Syntax-Free Developments. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{vanoostrom:LIPIcs.FSCD.2021.24,
  author =	{van Oostrom, Vincent},
  title =	{{Z; Syntax-Free Developments}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{24:1--24:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.24},
  URN =		{urn:nbn:de:0030-drops-142620},
  doi =		{10.4230/LIPIcs.FSCD.2021.24},
  annote =	{Keywords: rewrite system, confluence, normalisation, recurrence}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.32
Normalisation by Random Descent

Authors: Vincent van Oostrom and Yoshihito Toyama

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We present abstract hyper-normalisation results for strategies. These results are then applied to term rewriting systems, both first and higher-order. For example, we show hyper-normalisation of the left--outer strategy for, what we call, left--outer pattern rewrite systems, a class comprising both Combinatory Logic and the lambda-calculus but also systems with critical pairs. Our results apply to strategies that need not be deterministic but do have Newman's random descent property: all reductions to normal form have the same length, with Huet and Lévy's external strategy being an example. Technically, we base our development on supplementing the usual notion of commutation diagram with a notion of order, expressing that the measure of its right leg does not exceed that of its left leg, where measure is an abstraction of the usual notion of length. We give an exact characterisation of such global commutation diagrams, for pairs of reductions, by means of local ones, for pairs of steps, we dub Dyck diagrams.
Cite as

Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{vanoostrom_et_al:LIPIcs.FSCD.2016.32,
  author =	{van Oostrom, Vincent and Toyama, Yoshihito},
  title =	{{Normalisation by Random Descent}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.32},
  URN =		{urn:nbn:de:0030-drops-59862},
  doi =		{10.4230/LIPIcs.FSCD.2016.32},
  annote =	{Keywords: strategy, hyper-normalisation, commutation, random descent}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.174
Proof Orders for Decreasing Diagrams

Authors: Bertram Felgenhauer and Vincent van Oostrom

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
We present and compare some well-founded proof orders for decreasing diagrams. These proof orders order a conversion above another conversion if the latter is obtained by filling any peak in the former by a (locally) decreasing diagram. Therefore each such proof order entails the decreasing diagrams technique for proving confluence. The proof orders differ with respect to monotonicity and complexity. Our results are developed in the setting of involutive monoids. We extend these results to obtain a decreasing diagrams technique for confluence modulo.
Cite as

Bertram Felgenhauer and Vincent van Oostrom. Proof Orders for Decreasing Diagrams. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 174-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{felgenhauer_et_al:LIPIcs.RTA.2013.174,
  author =	{Felgenhauer, Bertram and van Oostrom, Vincent},
  title =	{{Proof Orders for Decreasing Diagrams}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{174--189},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.174},
  URN =		{urn:nbn:de:0030-drops-40616},
  doi =		{10.4230/LIPIcs.RTA.2013.174},
  annote =	{Keywords: involutive monoid, confluence modulo, decreasing diagram, proof order}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.240
Triangulation in Rewriting

Authors: Vincent van Oostrom and Hans Zantema

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We introduce a process, dubbed triangulation, turning any rewrite relation into a confluent one. It is more direct than usual completion, in the sense that objects connected by a peak are directly related rather than their normal forms. We investigate conditions under which this process preserves desirable properties such as termination.
Cite as

Vincent van Oostrom and Hans Zantema. Triangulation in Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 240-255, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{vanoostrom_et_al:LIPIcs.RTA.2012.240,
  author =	{van Oostrom, Vincent and Zantema, Hans},
  title =	{{Triangulation in Rewriting}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{240--255},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.240},
  URN =		{urn:nbn:de:0030-drops-34964},
  doi =		{10.4230/LIPIcs.RTA.2012.240},
  annote =	{Keywords: triangulation,codeterminism,completion,(co)confluence,(co)termination}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.5
Realising Optimal Sharing

Authors: Vincent van Oostrom

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Realising Optimal Sharing
Cite as

Vincent van Oostrom. Realising Optimal Sharing. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 5-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{vanoostrom:LIPIcs.RTA.2010.5,
  author =	{van Oostrom, Vincent},
  title =	{{Realising Optimal Sharing}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{5--6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.5},
  URN =		{urn:nbn:de:0030-drops-26403},
  doi =		{10.4230/LIPIcs.RTA.2010.5},
  annote =	{Keywords: Optimal Sharing}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.17
Higher-Order (Non-)Modularity

Authors: Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We show that, contrary to the situation in first-order term rewriting, almost none of the usual properties of rewriting are modular for higher-order rewriting, irrespective of the higher-order rewriting format. We show that for the particular format of simply typed applicative term rewriting systems modularity of confluence, normalization, and termination can be recovered by imposing suitable linearity constraints.
Cite as

Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen. Higher-Order (Non-)Modularity. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 17-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{appel_et_al:LIPIcs.RTA.2010.17,
  author =	{Appel, Claus and van Oostrom, Vincent and Simonsen, Jakob Grue},
  title =	{{Higher-Order (Non-)Modularity}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{17--32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.17},
  URN =		{urn:nbn:de:0030-drops-26427},
  doi =		{10.4230/LIPIcs.RTA.2010.17},
  annote =	{Keywords: Higher-order rewriting, modularity, termination, normalization}
}
  • Refine by Type
  • 16 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 4 2025
  • 1 2024
  • 2 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 8 van Oostrom, Vincent
  • 2 Heijltjes, Willem
  • 2 Hirokawa, Nao
  • 1 Abdul Hamid, Nadeem
  • 1 Accattoli, Beniamino
  • Show More...

  • Refine by Series/Journal
  • 16 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Lambda calculus
  • 1 Theory of computation
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 3 confluence
  • 3 lambda-calculus
  • 2 computational effects
  • 1 Coq
  • 1 Dependency pairs
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact