傑出學者系列講座: Coq, a Proof Assistant Based On Type Theory

資科所今年開始舉辦中研院資科所傑出學者系列講座,希望把各領域頂尖的學者請來台灣和本地研究者交流。十月將邀請法國 INRIA 教授,現在被請到北京清華的 Jean-Pierre Jouannaud:

摘要: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 的興趣是形式方法、定理證明、和軟體驗證等等。很難得的機會,有興趣的朋友可好好把握。

其他講者和時間請參考中研院資科所傑出學者系列講座網頁。

This entry was posted in 活動消息 and tagged , , . Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>