COEセミナーのお知らせ
For the information in English, please see the bottom of this message.
平成１９年１２月４日
関係各位
２１世紀COEプログラム
－検証進化可能電子社会－
拠点リーダー 片 山 卓 也
ＣＯＥセミナーの開催について
来る１２月１１日（火）に、下記のとおりＣＯＥセミナーを開催致します。
つきましては、多数の皆様にご参加いただきたく、ここにセミナーの案内を
申し上げます。
本セミナーに関しましては参加申し込み・予約等は必要ございませんので
直接、会場にお越しくださいますようよろしくお願い致します。
本セミナーは本日午前中に情報科学研究科 二木厚吉教授より案内が
ありました ==Jean-Pierre Jouannaud教授セミナーのお知らせ== と
同じセミナーです。
また、場所が変更となっておりますのでご確認お願いいたします。
記
日時 平成１９年１２月１１日（火） １５：００～１７：００
場所 情報科学研究科研究棟 Ⅲ棟５Ｆコラボレーションルーム６
講演題目 The Calculus of Congruent Inductive Constructions
講演者 Jean-Pierre Jouannaud (Ecole Polytechnique and INRIA)
講演要旨:
It is commonly agreed that the success of future proof assistants
will rely on their ability to incorporate computations within
deductions in order to mimic the mathematician when replacing the
proof of a proposition P by the proof of an equivalent proposition
P' obtained from P thanks to possibly complex calculations.
In this paper, we investigate a new version of the calculus of
inductive constructions which incorporates arbitrary decision
procedures into deductions via the conversion rule of the
calculus. Besides the novelty of the problem itself in the context
of the calculus of inductive constructions, a major technical
innovation of this work lies in the fact that the computation
mechanism varies along proof-checking: goals are sent to the
decision procedure together with the set of user hypotheses
available from the current context. Our main result shows that this
extension of the calculus of constructions does not compromise its
main properties: confluency, strong normalization and decidability
of proof-checking are all preserved.
担当教員：情報科学研究科 教授 二木 厚吉
問合せ先 安心電子社会研究センター （内線：1261・E-mail:coe-trust)
---------------------------------------
We would like to inform you about COE-Seminar as follows.
DATE : December 11, 2007 15:00-17:00
PLACE : IS Collaboration room 6 (IS Ⅲ-5F)
TITLE: The Calculus of Congruent Inductive Constructions
SPEAKER : Jean-Pierre Jouannaud (Ecole Polytechnique and INRIA)
REFERENCE: Research Center for trustworthy e-Society (E-mail: coe-trust)
平成１９年１２月４日
関係各位
２１世紀COEプログラム
－検証進化可能電子社会－
拠点リーダー 片 山 卓 也
ＣＯＥセミナーの開催について
来る１２月１１日（火）に、下記のとおりＣＯＥセミナーを開催致します。
つきましては、多数の皆様にご参加いただきたく、ここにセミナーの案内を
申し上げます。
本セミナーに関しましては参加申し込み・予約等は必要ございませんので
直接、会場にお越しくださいますようよろしくお願い致します。
本セミナーは本日午前中に情報科学研究科 二木厚吉教授より案内が
ありました ==Jean-Pierre Jouannaud教授セミナーのお知らせ== と
同じセミナーです。
また、場所が変更となっておりますのでご確認お願いいたします。
記
日時 平成１９年１２月１１日（火） １５：００～１７：００
場所 情報科学研究科研究棟 Ⅲ棟５Ｆコラボレーションルーム６
講演題目 The Calculus of Congruent Inductive Constructions
講演者 Jean-Pierre Jouannaud (Ecole Polytechnique and INRIA)
講演要旨:
It is commonly agreed that the success of future proof assistants
will rely on their ability to incorporate computations within
deductions in order to mimic the mathematician when replacing the
proof of a proposition P by the proof of an equivalent proposition
P' obtained from P thanks to possibly complex calculations.
In this paper, we investigate a new version of the calculus of
inductive constructions which incorporates arbitrary decision
procedures into deductions via the conversion rule of the
calculus. Besides the novelty of the problem itself in the context
of the calculus of inductive constructions, a major technical
innovation of this work lies in the fact that the computation
mechanism varies along proof-checking: goals are sent to the
decision procedure together with the set of user hypotheses
available from the current context. Our main result shows that this
extension of the calculus of constructions does not compromise its
main properties: confluency, strong normalization and decidability
of proof-checking are all preserved.
担当教員：情報科学研究科 教授 二木 厚吉
問合せ先 安心電子社会研究センター （内線：1261・E-mail:coe-trust)
---------------------------------------
We would like to inform you about COE-Seminar as follows.
DATE : December 11, 2007 15:00-17:00
PLACE : IS Collaboration room 6 (IS Ⅲ-5F)
TITLE: The Calculus of Congruent Inductive Constructions
SPEAKER : Jean-Pierre Jouannaud (Ecole Polytechnique and INRIA)
REFERENCE: Research Center for trustworthy e-Society (E-mail: coe-trust)
