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 Algebraic Functional Systems

Invited Speaker

  • Zhenjiang Hu (National Institute of Informatics, Japan)
    Can Graph Transformation be Bidirectionalized? -- Bidirectional Semantics of Structural Recursion on Graphs -- Abstract

Program

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

Proceedings

    The proceedings of HOR 2012 are here, 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.

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

Program Committee

Program and Organizing Chair

Further Information

See the HOR series.