• Vincent van Oostrom
    Z
    Syntax-Free Developments

    Draft paper, 22pp., 22 February, 2021, Accepted for presentation at FSCD 2021
    (abstract, PDF of draft, PDF in proceedings, slides of talk (pdf), pre-recorded talk (mp4), recorded live talk (mp4))

  • Vincent van Oostrom
    Multi-redexes and multi-treks induce residual systems
    least upper bounds and left-cancellation up to homotopy

    13 June, 2021, Accepted for presentation at IWC 2021
    (abstract, PDF of 7pp. IWC abstract, slides of talk (pdf), PDF of 15pp. version with proofs, recorded live talk (mp4))

  • Vincent van Oostrom
    Some symmetries of commutation diamonds
    IWC 2020, 5 pages, 30 June 2020
    (abstract, PDF, slides, video (MKV))

  • Vincent van Oostrom
    Decreasing proof orders
    Interpreting conversions in involutive monoids

    Draft paper, 17pp., 19 April, 2012
    and talks at TeReSe, Utrecht, Friday 9 December, 2011 and International Workshop on Confluence (IWC), Nagoya, Tuesday 29 May, 2012
    (abstract, PDF of a draft, PDF of TeReSe talk, PDF of IWC talk)

  • Vincent van Oostrom and Hans Zantema
    Triangulation in rewriting
    Draft paper, accepted for presentation at RTA 2012 and inclusion in its LIPIcs proceedings, October 2011 - January 2012
    and Talk at TeReSe, Eindhoven, Friday 17 June, 2011
    (abstract, PDF of final version, 16 pp, PDF in LGPS, 17 pp (local copy), PDF of talk)

  • Jörg Endrullis, Clemens Grabmayer, Jan Wiilem Klop, and Vincent van Oostrom
    On equal μ-terms
    Theoretical Computer Science, Volume 412, No. 28, pp. 3175-3202, 2011
    Festschrift in Honour of Jan Bergstra
    (abstract, PDF at Elsevier (local copy), PDF of talk)

  • Confluence via Critical Valleys
    Draft, UU, 2 pages, April 2011 and talk at 6th International Workshop on Higher-Order Rewriting (HOR 2012), Nagoya, Saturday 2 June, 2012
    (PDF, PDF of HOR talk)

  • Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen
    Higher-Order (Non-)Modularity
    Proceedings of the 21st RTA (RTA 2010), Edinburgh, July 2010, pp. 17-32, LIPIcs 6, Schloss Dagstuhl-Leibniz-Zentrum für Informatik
    and Logic Group Preprint Series 284, July 2010, 26 pp., Utrecht University (abstract, PDF in LIPIcs (local copy), PDF in LGPS (local copy), PDF of talk)

  • Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom
    Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
    Proceedings of the 21st RTA (RTA 2010), Edinburgh, July 2010, pp. 85-102, LIPIcs 6, Schloss Dagstuhl-Leibniz-Zentrum für Informatik
    (abstract, PDF in LIPIcs (local copy))

  • Clemens Grabmayer, Joop Leo, Vincent van Oostrom, and Albert Visser
    On the termination of Russell's description elimination algorithm
    The Review of Symbolic Logic, Volume 4, Number 3, pp. 367-393, September 2011, Cambridge University Press or Association for Symbolic Logic
    and Logic Group Preprint Series 280, 26 pp., November 2009, ZENO, Utrecht University
    (abstract, PDF in RSL (local copy), PDF in LGPS (local copy))

  • Vincent van Oostrom
    Abstract Rewriting
    3rd International School on Rewriting ISR 2008, Obergurgl, Austria, July 21-26, 2008
    Lecture 1, monday 21 July, 2008: confluence, lower bounds (part 1: decreasing diagrams, part 2: Z-property)
    Lecture 2, wednesday 23 July, 2008: orthogonality, greatest lower bounds (residual systems)
    including exercises (and one solution)

  • Vincent van Oostrom
    Modularity of Confluence, Constructed
    Proceedings of the 4th IJCAR (IJCAR 2008), Sydney, August 2008, pp. 348-363, LNCS 5195, Springer
    and Talk, IJCAR, Sydney, 14 August, 2008
    (abstract, PDF at Springer (local copy), PDF of talk)
    (Java tool developed by Marieke Peeters, february 2010)

  • Vincent van Oostrom
    Confluence by Decreasing Diagrams, Converted
    Proceedings of the 19th RTA (RTA 2008), Hagenberg, July 2008, pp. 306-320, LNCS 5117, Springer
    and Talk, RTA, Hagenberg 17 July, 2008
    (abstract, PDF at Springer (local copy), PDF of talk)

  • From sorting via braids, self-distributivity, and the substitution lemma of the lambda-calculus, to multisets.
    PPS, Paris, 31 January, 2008
    (PDF of talk)

  • Patrick Dehornoy and Vincent van Oostrom
    Z
    (Talk, PAM, CWI, 28 May 2008, Talk, LMRC 08, Moscow, 6 May 2008, Talk, LIX, Paris, 1 February 2008, Talk, Terese, Aachen, 28 November, 2007)

  • Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer
    Lambda Calculus with Patterns
    Theoretical Computer Science, Volume 398, Issues 1-3, 28 May 2008, pages 16-31, Elsevier
    (abstract, PDF at Elsevier)

  • Names in Higher-Order Rewriting
    Presentation at the ICMS workshop on Mathematical Theories of Abstraction, Substitution and Naming in Computer Science, May 26, 2007.
    (PDF)

  • Vincent van Oostrom
    Random Descent
    Proceedings of the 18th RTA (RTA 2007), Paris, June 2007, pp. 314-328, LNCS 4533, Springer
    and Talk, November 13 2007, FING, Montevideo
    (abstract, PDF at Springer, PDF of talk)

  • Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk
    Reduction Strategies and Acyclicity
    Rewriting, Computation and Proof: Essays Dedicated to Jean-Pierre Jouannaud on the Occassion of His 60th Birthday, 2007, pp. 89-112, LNCS 4600, Springer.
    (abstract, PDF at Springer)

  • Constructing Confluence
    Obergurgl, 8 September, 2006
    (PDF of talk)

  • Vincent van Oostrom
    Properties of Needed Strategies
    International School on Rewriting, LORIA, Nancy, France, July 3-7, 2006

  • Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer
    Iterative Lexicographic Path Orders
    Algebra, Meaning and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pp. 541 - 554, LNCS 4060, Springer
    (abstract, PDF at Springer)

  • Preponement
    Draft, UU, 2 pages, April 24th, 2011
    (abstract, PDF)

  • Counterexamples to Higher-Order Modularity
    Draft version 1.2, UU, 10 pages, 31 October, 2005
    (abstract, PDF, Obergurgl'05 (unfinished slides of) Talk)

  • Sorting vs. Braids vs. The Substitution Lemma vs. lambda xc
    Draft, UU, 7 pages, 11 October, 2005
    (abstract, PDF)

  • Vincent van Oostrom
    Acyclicity is Modular for Orthogonal TRSs
    Draft version 1.1, UU, 2 pages, 26 July, 2005
    (abstract, PDF)

  • Vincent van Oostrom
    Newman's Proof of Newman's Lemma
    Draft, UU, 2 pages, 25 July, 2005
    (abstract, PDF)

  • Vincent van Oostrom
    Explicit substitution for graphs
    UU, Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica, nummer 9, pp. 34-39, 2005
    (abstract, PDF)

  • Jeroen Ketema, Jan Willem Klop, and Vincent van Oostrom
    Vicious Circles in Rewriting Systems
    UU, 55 pages, 29 December, 2004
    (abstract, CKI Preprint 52, CWI Report SEN-E0427, WRS'05 Participant's proceedings (20 pages), WRS'05 Talk)

  • Vincent van Oostrom
    Delimiting Diagrams (superseded by Random Descent )
    UU/UEA Norwich/FING, 3 pages, July-December, 2004
    (abstract, CKI Preprint 53)

  • Jeroen Ketema, Jan Willem Klop, and Vincent van Oostrom
    Vicious Circles in Orthogonal Term Rewriting Systems
    CWI, Report SEN-R0418, ISSN 1386-369X, 13 pages, December, 2004
    (abstract, PDF)

  • Vincent van Oostrom (ed.)
    Rewriting Techniques and Applications
    15th International Conference, RTA 2004
    Aachen, Germany, June 2004
    Proceedings

    LNCS 3091, Springer, ISBN 3-540-22153-0
    (Springer ordering page, online)

  • Vincent van Oostrom, Kees-Jan van de Looij, Marijn Zwitserlood
    ] (lambdascope)
    Workshop on Algebra and Logic on Programming Systems (ALPS), Kyoto, April 10th 2004
    (talk, extended abstract postscript, PDF)
    (slides of a talk by Jeroen Goudsmit, january 2010)
    (Haskell tool developed by Paul Liu, september 2009)

  • Terese
    Term Rewriting Systems
    Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press, 906 pages, March 2003. ISBN 0521391156
    (abstract, CUP ordering page)

  • Dimitri Hendriks and Vincent van Oostrom
    Adbmal
    Proceedings of the 19th Conference on Automated Deduction (CADE 19), Miami, July-August 2003, pp. 136 - 150, LNAI 2741
    (abstract, PDF at Springer, submitted journal version, Coq proofs prerelease, talk ZIC 11-2-2003)

  • Vincent van Oostrom
    A simple rewrite proof of the equational interpolation theorem
    CWI, Draft, 1 page, 1 January, 2003
    (abstract, postscript, PDF)

  • Vincent van Oostrom and Roel de Vrijer
    Four equivalent equivalences of reductions
    Invited paper for special issue of ENTCS, volume 70, issue 6, on WRS'02, pages 21-61, 5 December, 2002
    (abstract, PDF at Elsevier)

  • Sander Bruggink, Dimitri Hendriks, Vincent van Oostrom, Roel de Vrijer
    Optimal Implementation of Higher-Order Rewriting
    Joint invited talk for HOR/ WRS, 56 pages, 21 July, 2002
    (abstract, pdf)

  • Vincent van Oostrom
    Trivial
    UU, Draft, 1 page, August 1998
    (abstract, postscript, pdf)

  • Zurab Khasidashvili, Mizuhito Ogawa, and Vincent van Oostrom
    Uniform Normalisation beyond Orthogonality
    Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA '01), Utrecht, May 2001, pp. 122 - 136, LNCS 2051, Springer
    (abstract)

  • Vincent van Oostrom
    Sub-Birkhoff
    Proceedings of the 7th International Symposium on Functional and Logic Programming (FLOPS 2004), Nara, April 2004, pp. 180-195, LNCS 2998, Springer
    (abstract, talk 8-8-2004)

  • Vincent van Oostrom
    A one rule term rewrite system which is UN but not UN->
    UU, Puzzle, 1/3 page, 1997
    (abstract, postscript)

  • Vincent van Oostrom
    S-terms can eat at most three passive arguments
    UU, A proof to [A.Visser, 1981, PhD UU, Stelling 12], 1/3 page, February 2000
    (abstract, postscript)

  • Sugwoo Byun, Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries
    Separability and translatability of sequential term rewrite systems into the lambda calculus
    Submitted, 26 pages, 3 December, 1999
    (abstract, postscript)

  • Vincent van Oostrom
    Reduce to the max
    UU & CWI, Draft, 1 page, July 1999
    (abstract, PDF, postscript)

  • Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries
    Meaningless Terms in Rewriting
    The Journal of Functional and Logic Programming, Volume 1999, Article 1, 35 pages, 16 February, 1999
    (abstract, The MIT Press, electronic version (Muenster, Germany))

  • Zurab Khasidashvili, Mizuhito Ogawa, and Vincent van Oostrom
    Perpetuality and Uniform Normalization
    in Orthogonal Rewrite Systems

    Information and Computation, Volume 164, pp. 118 - 151, 2001
    (abstract)

  • Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer
    A geometric proof of confluence by decreasing diagrams
    Journal of Logic and Computation, Volume 10, No. 3, pp. 437 - 460, June 2000
    (abstract, Oxford University Press, PDF version (UK))

  • Vincent van Oostrom
    Normalisation in weakly orthogonal rewriting
    Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA '99), Trento, July 1999, pp. 60 - 74, LNCS 1631
    (abstract, Springer, PDF version (Germany))

  • Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer
    Course Notes on Braids
    UU & CWI, Draft, 45 pages, July 1998
    (abstract, postscript, PDF)

  • Vincent van Oostrom
    Eventually Increasing
    UU & CWI, Draft, 1 page, April 1998
    (abstract, postscript)

  • Marc Bezem, Vincent van Oostrom, and Jan Willem Klop
    Diagram Techniques for Confluence
    Information and Computation, Volume 141, No. 2, pp. 172 - 204, March 15, 1998
    (abstract)

  • Jan Willem Klop, Vincent van Oostrom, Roel de Vrijer
    Herschrijftechnieken voor Vlechten
    VU, Amsterdam, Klad, 45 bladzijden, Augustus 1997
    (abstract, postscript)

  • Vincent van Oostrom
    A Splitting Headache
    VU, Amsterdam, Draft, 1 page, July 1997
    (abstract, postscript)

  • Vincent van Oostrom
    Finite Family Developments
    Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA '97), Sitges, June 1997, pp. 308 - 322, LNCS 1232
    (abstract, PDF at Springer (DOI: 10.1007/3-540-62950-5_80) (local copy), preliminary version)

  • Vincent van Oostrom
    Developing Developments
    Theoretical Computer Science, Volume 175, No. 1, pp. 159 - 181, March 30, 1997
    (abstract, technical report)

  • Vincent van Oostrom
    FD à la Melliès
    VU, Amsterdam, Draft, 4 pages, February 1997
    (abstract, postscript)

  • Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries
    Meaningless Terms in Rewriting
    Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP '96), Aachen, September 1996, pp. 254 - 268, LNCS 1139
    (abstract)

  • Vincent van Oostrom
    Higher-Order Families
    Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA '96), New Brunswick, July 1996, pp. 392 - 407, LNCS 1103
    (abstract, preliminary version)

  • Vincent van Oostrom
    Take five
    Technical Report IR-406, Vrije Universiteit, Amsterdam, 10 pages, June 5, 1996
    (abstract, compressed postscript (VU, Amsterdam))

  • Vincent van Oostrom
    Development Closed Critical Pairs
    Proceedings of the 2nd International Workshop on Higher-Order Algebra, Logic, and Term Rewriting (HOA '95), Paderborn, September 1995, pp. 185 - 200, LNCS 1074
    (abstract, participants proceedings version)

  • Zurab Khasidashvili and Vincent van Oostrom
    Context-sensitive Conditional Expression Reduction Systems
    Electronic Notes in Theoretical Computer Science, Volume 2, Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation (SEGRAGRA '95), Volterra, August 1995
    (abstract, technical report (UEA, Norwich))

  • Vincent van Oostrom and Femke van Raamsdonk
    Weak orthogonality implies confluence:
    the higher-order case

    Proceedings of the 3rd International Symposium on Logical Foundations of Computer Science (LFCS '94), St. Petersburg, June 1994, pp. 379 - 392, LNCS 813
    (abstract, doi:10.1007/3-540-58140-5_35, technical report)

  • Vincent van Oostrom
    Confluence by Decreasing Diagrams
    Theoretical Computer Science, Volume 126, No. 1, pp. 259 - 280, April 25, 1994
    (abstract, technical reports 1, 2 (VU, Amsterdam))

  • Vincent van Oostrom
    Confluence for Abstract and Higher-Order Rewriting
    PhD thesis, Vrije Universiteit, Amsterdam, 146 pages, March 29, 1994
    (abstract, postscript)

  • Vincent van Oostrom and Erik de Vink
    Transition system specifications in stalk format with bisimulation as a congruence
    Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science (STACS '94), Caen, February 1994, pp. 569 - 580, LNCS 775
    (abstract, technical report (VU, Amsterdam))

  • Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk
    Combinatory Reduction Systems: introduction and survey
    Theoretical Computer Science, Volume 121, No. 1 & 2, pp. 279 - 308, December 1993
    (abstract, doi:10.1016/0304-3975(93)90091-7, VU technical report IR-327 PS.Z, PDF)

  • Vincent van Oostrom and Femke van Raamsdonk
    Comparing Combinatory Reduction Systems and Higher-Order Rewrite Systems
    Proceedings of the International Workshop on Higher-Order Algebra, Logic, and Term Rewriting (HOA '93), Amsterdam, September 1993, pp. 276 - 304, LNCS 816
    (abstract, technical report (VU, Amsterdam))

  • Vincent van Oostrom
    Lambda Calculus with Patterns
    Technical Report IR-228, Vrije Universiteit, Amsterdam, 40 pages, November 1990
    (abstract, VU technical report IR-228 PS.Z, PDF)