{"id":6697,"date":"2023-10-30T13:00:00","date_gmt":"2023-10-30T22:00:00","guid":{"rendered":"https:\/\/prg.is.titech.ac.jp\/?p=6697"},"modified":"2025-03-06T14:18:52","modified_gmt":"2025-03-06T23:18:52","slug":"3-talks-on-formalization-at-tpp-2023","status":"publish","type":"post","link":"https:\/\/prg.is.titech.ac.jp\/ja\/news\/3-talks-on-formalization-at-tpp-2023\/","title":{"rendered":"\u5ddd\u6dfb\u3001\u6589\u85e4\u3001\u6d25\u5c71\u304c\u5b9a\u7406\u8a3c\u660e\u652f\u63f4\u7cfb\u3092\u4f7f\u3063\u305f\u7814\u7a76\u3092TPP 2023\u306b\u3066\u767a\u8868"},"content":{"rendered":"<p>\u5ddd\u6dfb\u88d5\u529f\" target=\"_blank\" rel=\"noopener\">Kawazoe<\/a>, <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/ayumu-saito\/\" data-internallinksmanager029f6b8e52c=\"314\" title=\"Ayumu Saito\" target=\"_blank\" rel=\"noopener\">Saito<\/a> and <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/syouki-tsuyama\/\" data-internallinksmanager029f6b8e52c=\"317\" title=\"Syouki Tsuyama\" target=\"_blank\" rel=\"noopener\">Tsuyama<\/a> presented their ongoing studies that use theorem provers at <a href=\"https:\/\/aabaa.github.io\/tpp2023\/\">The 19th Theorem Proving and Provers meeting<\/a>. Interestingly, they all use different systems (Lean, Coq and Agda). The 19th Theorem Proving and Provers meeting\u306b\u3066<a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/kawazoe\/\" data-internallinksmanager029f6b8e52c=\"330\" title=\"\u5ddd\u6dfb\u88d5\u529f\" target=\"_blank\" rel=\"noopener\">\u5ddd\u6dfb<\/a>\u3001<a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/ayumu-saito\/\" data-internallinksmanager029f6b8e52c=\"314\" title=\"Ayumu Saito\" target=\"_blank\" rel=\"noopener\">\u6589\u85e4<\/a>\u3001<a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/syouki-tsuyama\/\" data-internallinksmanager029f6b8e52c=\"317\" title=\"Syouki Tsuyama\" target=\"_blank\" rel=\"noopener\">\u6d25\u5c71<\/a>\u304c\u5b9a\u7406\u8a3c\u660e\u652f\u63f4\u7cfb\u3092\u4f7f\u3063\u305f\u7814\u7a76\u306b\u3064\u3044\u3066\u767a\u8868\u3057\u307e\u3059\u3002\u305d\u308c\u305e\u308cLean, Coq, Agda\u3092\u4f7f\u3063\u3066\u3044\u3066\u3001\u5b9a\u7406\u8a3c\u660e\u652f\u63f4\u7cfb\u306e\u591a\u69d8\u6027\u306b\u3082\u6311\u6226\u3057\u3066\u3044\u307e\u3059 \ud83d\ude42 <\/p>\r\n\r\n\n<iframe src='\/papers\/bibindex.php?keys=kawazoe2023tpp,saito2023tpp,tsuyama2023tpp&bib=prg-e.bib;thesis-b.bib;thesis-m.bib;thesis-d.bib;prg-j.bib&parent=%2Fja%2Fwp-json%2Fwp%2Fv2%2Fposts%2F6697' class='bibtexbrowser' onload='resizeIframe(this)'><\/iframe>\n<iframe id='kawazoe2023tpp' src='\/papers\/bibtexbrowser.php?key=kawazoe2023tpp&bib=prg-e.bib;thesis-b.bib;thesis-m.bib;thesis-d.bib;prg-j.bib' class='bibtexbrowser' onload='resizeIframe(this)'><\/iframe>\n<iframe id='saito2023tpp' src='\/papers\/bibtexbrowser.php?key=saito2023tpp&bib=prg-e.bib;thesis-b.bib;thesis-m.bib;thesis-d.bib;prg-j.bib' class='bibtexbrowser' onload='resizeIframe(this)'><\/iframe>\n<iframe id='tsuyama2023tpp' src='\/papers\/bibtexbrowser.php?key=tsuyama2023tpp&bib=prg-e.bib;thesis-b.bib;thesis-m.bib;thesis-d.bib;prg-j.bib' class='bibtexbrowser' onload='resizeIframe(this)'><\/iframe>\r\n<!-- \/wp:post-content -->","protected":false},"excerpt":{"rendered":"<p>\u5ddd\u6dfb\u88d5\u529f&#8221; target=&#8221;_blank&#8221; rel=&#8221;noopener&#8221;>Kawazoe, Saito and Tsuyama presented their ongoing studies that use theor&hellip; <a class=\"continue\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/3-talks-on-formalization-at-tpp-2023\/\">Continue Reading \u5ddd\u6dfb\u3001\u6589\u85e4\u3001\u6d25\u5c71\u304c\u5b9a\u7406\u8a3c\u660e\u652f\u63f4\u7cfb\u3092\u4f7f\u3063\u305f\u7814\u7a76\u3092TPP 2023\u306b\u3066\u767a\u8868<\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"nf_dc_page":"","_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[36,29,5],"tags":[],"class_list":["post-6697","post","type-post","status-publish","format-standard","hentry","category-intrinsically-typed-interpreters","category-monae","category-news","radius"],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/posts\/6697","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/comments?post=6697"}],"version-history":[{"count":10,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/posts\/6697\/revisions"}],"predecessor-version":[{"id":9467,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/posts\/6697\/revisions\/9467"}],"wp:attachment":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/media?parent=6697"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/categories?post=6697"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/tags?post=6697"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}