International Workshop on Higher-Order Rewriting

HOR 2023 – 11th International Workshop on Higher-Order Rewriting

Rome, Italy
4 July 2023
affiliated with FSCD 2023 and CADE-29

Home — Overview — Submission — Important dates — Invited speaker — Proceedings — Preliminary programme — Committees

Overview

HOR is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress. The following is a non-exhaustive list of topics for the workshop:

Applications: proof checking, theorem proving, generic programming, declarative programming, program transformation, automated termination/confluence/equivalence analysis tools.
Foundations: pattern matching, unification, strategies, narrowing, termination, syntactic properties, type theory, complexity of derivations.
Frameworks: term rewriting, conditional rewriting, graph rewriting, net rewriting, comparisons of different frameworks.
Implementation: explicit substitution, rewriting tools, compilation techniques.
Semantics: semantics of higher-order rewriting, categorical rewriting, higher-order abstract syntax, games and rewriting

Information about previous editions can be found here.

Information about registration can be found here (early registration deadline: 31 May 2023).

Submission

To give a presentation at the workshop, please submit an extended abstract (between 2 to 5 pages) via Easychair:

https://easychair.org/conferences/?conf=hor2023

Please use LaTeX and the Easychair style to prepare your submission:

https://easychair.org/publications/easychair.zip

HOR is a platform for discussing open questions, ongoing research, and new perspectives, as well as new results. Extended abstracts describing work in progress, preliminary results, research projects, or problems in higher-order rewriting are very welcome. Specifically, short versions of recently published papers are welcome, and submission to HOR does not preclude formal publication at other venues.

The workshop has informal electronic proceedings that will be made available on this website.

For questions regarding submission, please contact the PC chair Carsten Fuhs.

Important dates

Submission deadline: ~~2 May 2023~~ extended: 9 May 2023
Notification: 29 May 2023
Final version: 12 June 2023

All times are Anywhere on Earth.

Invited speaker

Pablo Barenbaum – Universidad de Buenos Aires, Argentina

Title: Quantitative Types for Useful Reduction

Proceedings

The Proceedings of HOR 2023 are now available.

Preliminary programme

Session 1

14:00 – Welcome
14:06 – Pablo Barenbaum (invited talk) – Quantitative Types for Useful Reduction
15:06 – Makoto Hamana – Modular Termination for Second-Order Rewriting Systems and Application to Effect Handlers

Coffee break

15:30 – Coffee break

Session 2

16:00 – Cynthia Kop, Deivid Vale and Niels van der Weide – Nijn/Onijn: A New Certification Engine for Higher-Order Termination
16:24 – Liye Guo and Cynthia Kop – Higher-Order LCTRSs and Their Termination
16:48 – Thiago Felicissimo – Confluence Criterion for Non Left-Linearity in a Beta/Eta-Free Reformulation of HRSs
17:12 – Victor Arrial – A Deeper Study of λ!-Calculus Simulations
17:36 – Axel Kerinec and Lionel Vaux Auclair – The algebraic lambda-calculus is a conservative extension of the ordinary lambda-calculus

Committees

Programme Committee:

Takahito Aoto – Niigata University, Japan
Maribel Fernández – King's College London, United Kingdom
Carsten Fuhs (Chair) – Birkbeck, University of London, United Kingdom
Delia Kesner – Université Paris Cité, France
Cynthia Kop – Radboud Universiteit Nijmegen, The Netherlands
Damiano Mazza – Université Paris 13, France

Steering Committee:

Delia Kesner – Université Paris Cité, France
Femke van Raamsdonk – Vrije Universiteit Amsterdam, The Netherlands