[logic-ml] Call for Participation: HOR'12, Nagoya

[Makoto Hamana]

皆様、

今月末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