HOR 2012

6th International Workshop on Higher-Order Rewriting

June 2, 2012, Nagoya
Colocated with RTA'12

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 concerning higher-order rewriting.
The following is a non-exhaustive list of topics for the workshop:
  • Applications: proof checking, type checking, theorem proving, functional programming, declarative programming, program transformation, using some notions of higher-order rewriting.
  • Foundations: pattern matching, unification, strategies, termination, syntactic properties, type theory, for higher-order rewriting.
  • Frameworks: graph rewriting, net rewriting, comparisons of different formats.
  • Implementation: explicit substitution, rewriting tools, compilation techniques.
  • Semantics: semantics of higher-order rewriting, higher-order abstract syntax, categorical rewriting.

Accepted papers

  • Category B
    • Beniamino Accattoli and Delia Kesner: The permutative lambda-calculus (extended abstract)
      (The original paper was presented at LPAR'12, LNCS 7180, pp.381-395)
    • Thibaut Balabonski: A Unified Approach to Fully Lazy Sharing
      (The original paper was presented at POPL'12, pp.233-246)
  • Category A
    • Yuki Chiba and Takahito Aoto: Pattern Matching Algorithm for Higher Order Program Transformations
    • Jean-Pierre Jouannaud and Jian-Qi Li: Termination of higher-order rewriting in dependent type calculi
    • Vincent van Oostrom: Confluence via Critical Valleys
    • Kristoffer Rose: Higher Order Rewriting for Real Programmers

Special Session: Current Status of Higher-Order Termination Tools

This year's HOR has also a tool session. The following termination checkers for varieties of higher-order rewriting systems will be presented:
  • Carsten Fuhs: Haskell termination tool
  • Rene Thiemann: Isabelle termination tool
  • Aoto,Yamada: Simply-typed TRS termination tool
  • Cynthia Kop: WANDA, termination tool for AFS

Invited Speaker

Program (tentative)

  • 9:00 - 10:00 Invited talk
    • Zhenjiang Hu: Can Graph Transformation be Bidirectionalized?
      -- Bidirectional Semantics of Structural Recursion on Graphs --
  • 10:00 - 10:30 Coffee break
  • 10:30 - 12:00
    • Beniamino Accattoli and Delia Kesner: The permutative lambda-calculus
    • Thibaut Balabonski: A Unified Approach to Fully Lazy Sharing
    • Kristoffer Rose: Higher Order Rewriting for Real Programmers
  • 12:00 - 13:30 Lunch
  • 13:30 - 15:00
    • Yuki Chiba and Takahito Aoto: Pattern Matching Algorithm for Higher Order Program Transformations
    • Vincent van Oostrom: Confluence via Critical Valleys
    • Jean-Pierre Jouannaud and Jian-Qi Li: Termination of higher-order rewriting in dependent type calculi
  • 15:00 - 15:30 Coffee break
  • 15:30 - 16:20
    • Carsten Fuhs: Haskell termination tool
    • Rene Thiemann: Isabelle termination tool
  • 16:20 - 16:30 Short break
  • 16:30 - 17:20
    • Aoto,Yamada: Simply-typed TRS termination tool
    • Cynthia Kop: WANDA, termination tool for AFS

Submissions

    Two categories of papers are solicited:
    • Category A: Extended abstracts of new results, describing work in progress, or problems in higher-order rewriting.
    • Category B: Short versions of recently published or submitted elsewhere articles on higher-order rewriting. Papers in this category are for presentation only, and not considered as candidates for the post-workshop proceedings.
    Papers in both categories should be between 2 and 5 pages, and should note the category (either A or B). Papers are formatted according to EPTCS style, and submitted electronically via the EasyChair submission website. Papers will be judged on relevance, originality, correctness and usefulness.

    Please address your questions to the PC chair: hamana at cs.gunma-u.ac.jp.

Important dates

    Paper submission: March 29, 2012 23:00 (GMT) (closed)
    Notification: April 20, 2012
    Final version: May 10, 2012
    Workshop: June 2, 2012

Proceedings

    The proceedings of HOR 2012 will be made available on the HOR 2012 web page, and a printed version will be distributed at the workshop. Post-workshop proceedings of extended abstracts of selected contributions is planned to be published as a volume of EPTCS.

Program Committee

Program and Organizing Chair

Further Information

See the HOR series.