Mita Logic Seminar
Jean-Pierre Jouannaud 教授講演会

日時: 2006年10月17日 17:00〜

場所: 三田東宝ビル8F人文COE会議室(*場所等不明な方は慶大正門のガードマンにお尋ね下さい)

講演者: 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.

「心の統合的研究」センター ワークショップ事務局
住所:東京都港区三田 3-1-7 三田東宝ビル 8F
e-mail:philosophy at