• 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)