Waseda Institute for Advanced Study (WIAS)早稲田大学 高等研究所

News

ニュース

WIAS 主催セミナー: “Type Theory and Proof Theory” (3/16) 

WIAS 主催セミナー: “Type Theory and Proof Theory”(3/16)

講演者 / Speaker

XU, Chuangjie (博士研究員, Ludwig-Maximilians-Universität München)
山﨑 紗紀子  (博士課程, 首都大学東京)

プログラム / Schedule

講演および質疑応答 (1) 13:20~14:20
講演者:XU, Chuangjie

タイトル: The computer as referee in mathematics
アブストラクト: Proofs in modern mathematics now cover hundreds and soon thousands) of pages, with additional computer calculations worth gigabytes of data. Given that no referee (or even team of referees) can reliably judge the correctness of such a proof, how should mathematics as a field proceed? I will discuss one way forward, namely the use of Martin-Loef’s constructive type theory and the associated proof assistants (like Agda and Coq) to formalise and verify the correctness of proofs, and to execute proofs as computer programs. During the talk I will use the Agda proof assistant for demonstration.

講演および質疑応答 (2) 14:30~15:30
講演者:山﨑 紗紀子 (YAMASAKI, Sakiko)

タイトル:An attempt at a new embedding of intuitionistic logic into linear logic-via multi-succedent G3-style sequent calculus for intuitionistic logic-
アブストラクト:In this presentation, I will examine the relationship between linear logic and G3-style sequent calculus for intuitionistic logic. It is well known that intuitionistic logic can be embedded into linear logic (Girard embedding). It is natural to do so, because intuitionistic logic can be embedded into modal logic S4 (Gödel embedding), and the behavior of exponentials for linear logic (! and?) is similar to that of the modal operators for S4 ( and ◇). Here, it is important for us (1) which system of intuitionistic logic is to be adopted, and (2) that the proof of the embedding is properly proof-theoretic one. For this purpose, we would like to employ the multi-succedent cut-free G3-style sequent calculus for intuitionistic logic: G3Int. I have already shown that we can establish the proof-theoretic proof for Gödel embedding via G3Int. Now, how about Girard embedding? In this presentation, I will propose a new translation. And I shall investigate this matter. Furthermore, as far as I can, I will examine the relationship between Gödel embedding and Girard embedding.

References:
A.S. Troelstra. Lectures on Linear Logic, CSLI-Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.
A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. 2nd edn. Cambridge University Press, 2000.

会 場 / Venue

早稲田大学 早稲田キャンパス 26号館 11階 1102教室

主 旨 / Outline

In this seminar, we have two talks on the advanced research with respect to type theory and proof theory in mathematical logic.
The prospected audience are graduate students and researchers who have basic knowledge about them.

コーディネーター / Coordinator

藤原 誠    (早稲田大学 高等研究所 助教)
秋吉 亮太(早稲田大学 高等研究所 准教授)

対 象 / Prospected Audience

学部生・大学院生・教職員・一般

言 語 / Language

英語

主 催 / Organizer

早稲田大学  高等研究所

申込み / Registration

事前申込み不要です。直接会場にお越しください。

Dates
  • 0316

    FRI
    2018

Place

早稲田大学 早稲田キャンパス 26号館 11階 1102教室

Tags
Page Top
WASEDA University

早稲田大学オフィシャルサイト(https://www.waseda.jp/inst/wias/)は、以下のWebブラウザでご覧いただくことを推奨いたします。

推奨環境以外でのご利用や、推奨環境であっても設定によっては、ご利用できない場合や正しく表示されない場合がございます。より快適にご利用いただくため、お使いのブラウザを最新版に更新してご覧ください。

このままご覧いただく方は、「このまま進む」ボタンをクリックし、次ページに進んでください。

このまま進む

対応ブラウザについて

閉じる