日時： 2006年10月17日 17：00〜
場所：
三田東宝ビル８F人文COE会議室（＊場所等不明な方は慶大正門のガードマンにお尋ね下さい）
(JR田町駅または都営地下鉄三田駅または赤羽橋駅（大江戸線）から徒歩5分)
＊建物の入口が常時ロックされておりますので，ドア脇のインターホンにて7Fの事務室又は8Fをお呼び出し下さい．
講演者： Jean-Pierre Jouannaud (Laboratoire d'Infomatique, Ecole Polytechnique)
タイトル： Orderings for proving termination of higher-order calculi
アブストラクト： I will present the properties needed for orderings able to prove termination of higher-order rewrite rules in a higher-order calculus without dependent types. Since there are two possible kinds of rewrite rules, there are two kinds of orderings, depending wether beta and eta reductions are considered as rules (as in, e.g. Coq) or are built-in the pattern matching procedure (as in, e.g., in Isabelle) in which higher-order pattern matching is used to fire rules instead of first-order. I will then present HORPO as an ordering of the first kind, as well as a generic mecanism to transform any ordering of the first kind into an ordering of the second kind. Many examples will be provided, as well as a PROLOG implementation.
問合せ先：