資科所今年開始舉辦中研院資科所傑出學者系列講座，希望把各領域頂尖的學者請來台灣和本地研究者交流。十月將邀請法國 INRIA 教授，現在被請到北京清華的 Jean-Pierre Jouannaud：
- 主題: Coq, a Proof Assistant Based On Type Theory
- 主講人: Prof. Jean-Pierre Jouannaud
- 地點: 中央研究院資訊科學研究所 新館106演講廳
- 日期: 2009/10/16, 週五
- 時間: 10:00~12:00
摘要：I shall describe how the Curry-Howard isomorphism between types/propositions and programs/proofs leads to a natural architecture which is common to most proof assistants (PA) based on higher-order type theory. A main advantage of this architecture is that the correctness of proofs can be trusted provided a quite small part of the code of the whole PA — the kernel — is trusted. We shall then stress why the usual intensional equality available in type theory is not adequate for applications, propose a novel architecture allowing the integration of an extensional equality to type theory, and discuss why this novel architecture can again be trusted. Details about this new implementation of Coq shall be given in conclusion.
Jouannaud 的興趣是形式方法、定理證明、和軟體驗證等等。很難得的機會，有興趣的朋友可好好把握。
其他講者和時間請參考中研院資科所傑出學者系列講座網頁。