皆様、

今月末RTA併設の、高階書換系ワークショップHOR'12の参加ご案内です。

今年はスペシャルセッションとして、停止性自動検証ツールの最新成果 のセッションを設けました。特に応用として

- Haskell - Isabelle

のプログラムの停止性検証ツール、および高階書換え系の停止性ツール制 作者に、実装とその理論を発表していただきます。 また論文発表の一つには、IBMでの実際のコンパイラにおける高階書換え の応用プロジェクト(Kristoffer Rose氏)の話題などもあり、 関数型言語、定理証明系などの利用者にも有用な情報になると思いますの で、関連研究者の皆様は、ぜひ参加をご検討ください。

レギュラーレジストレーション〆切は明日5/9ですが、直接会場での参加 費払いも可能です。ワークショップのみでも参加可能で、でしたら当日で も参加費はほとんど変わりませんし、RTA参加者でしたら同じです。同日 併設のツリーオートマタのTTATTワークショップ登録の方は、両方参加で きますので、部分的な参加でも歓迎です。

-- 浜名 誠/群馬大学

===================================================================== Call for Participation 6th International Workshop on Higher-Order Rewriting

HOR 2012

June 2, 2012, Nagoya, Japan Colocated with RTA'12 http://www.cs.gunma-u.ac.jp/events/hor/ ======================================================================

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

Special Session: Current Status of Higher-Order Termination Tools ----------------------------------------------------------------- * Carsten Fuhs: Haskell termination tool * Rene Thiemann: Isabelle termination tool * Aoto,Yamada: Simply-typed TRS termination tool * Cynthia Kop: WANDA, termination tool for AFS

Accepted papers ---------------- * Beniamino Accattoli and Delia Kesner: The permutative lambda-calculus (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)

* 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