{"id":10560,"date":"2025-09-02T01:50:04","date_gmt":"2025-09-02T10:50:04","guid":{"rendered":"https:\/\/prg.is.titech.ac.jp\/?p=10560"},"modified":"2025-09-02T14:29:31","modified_gmt":"2025-09-02T23:29:31","slug":"lecture-on-agda-at-ppl-summer-school","status":"publish","type":"post","link":"https:\/\/prg.is.titech.ac.jp\/ja\/news\/lecture-on-agda-at-ppl-summer-school\/","title":{"rendered":"PPL \u30b5\u30de\u30fc\u30b9\u30af\u30fc\u30eb\u3067\u306e Agda \u306b\u95a2\u3059\u308b\u8b1b\u6f14"},"content":{"rendered":"<p>\u53e2\u60a0\u60a0\" target=\"_blank\" rel=\"noopener\">Cong<\/a> will give a lecture on dependently typed programming in Agda at PPL Summer School 2025, affiliated with the 42nd JSSST annual conference.<\/p>\n<p>The materials for the lecture can be found on <a href=\"https:\/\/github.com\/YouyouCong\/pplss-2025\">GitHub<\/a>.<\/p>\n<p> <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/cong\/\" data-internallinksmanager029f6b8e52c=\"298\" title=\"\u53e2\u60a0\u60a0\" target=\"_blank\" rel=\"noopener\">\u53e2<\/a>\u304c\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u79d1\u5b66\u4f1a\u7b2c42\u56de\u5927\u4f1a\u306b\u4f75\u8a2d\u3055\u308c\u3066\u884c\u308f\u308c\u308b PPL \u30b5\u30de\u30fc\u30b9\u30af\u30fc\u30eb 2025 \u3067\u3001Agda \u306b\u3088\u308b\u4f9d\u5b58\u578b\u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0\u306b\u95a2\u3059\u308b\u8b1b\u6f14\u3092\u884c\u3044\u307e\u3059\u3002<\/p>\n<p>\u8b1b\u6f14\u8cc7\u6599\u306f <a href=\"https:\/\/github.com\/YouyouCong\/pplss-2025\">GitHub<\/a> \u3067\u516c\u958b\u3055\u308c\u3066\u3044\u307e\u3059\u3002<\/p>\n<p><\/p>\n<p><a href=\"https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?ssl=1\"><img data-recalc-dims=\"1\" decoding=\"async\" loading=\"lazy\" class=\"alignnone size-medium wp-image-10651\" src=\"https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?resize=300%2C225&#038;ssl=1\" alt=\"\" width=\"300\" height=\"225\" srcset=\"https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?resize=300%2C225&amp;ssl=1 300w, https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?resize=1024%2C768&amp;ssl=1 1024w, https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?resize=768%2C576&amp;ssl=1 768w, https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?w=1417&amp;ssl=1 1417w, https:\/\/i0.wp.com\/prg.is.titech.ac.jp\/wp-content\/uploads\/2025\/09\/IMG_9399-1.jpg?w=1120&amp;ssl=1 1120w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><\/p>","protected":false},"excerpt":{"rendered":"<p>\u53e2\u60a0\u60a0&#8221; target=&#8221;_blank&#8221; rel=&#8221;noopener&#8221;>Cong will give a lecture on dependently typed programming in Agda at PPL S&hellip; <a class=\"continue\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/lecture-on-agda-at-ppl-summer-school\/\">Continue Reading PPL \u30b5\u30de\u30fc\u30b9\u30af\u30fc\u30eb\u3067\u306e Agda \u306b\u95a2\u3059\u308b\u8b1b\u6f14<\/a><\/p>\n","protected":false},"author":6,"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":[5],"tags":[],"class_list":["post-10560","post","type-post","status-publish","format-standard","hentry","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\/10560","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\/6"}],"replies":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/comments?post=10560"}],"version-history":[{"count":5,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/posts\/10560\/revisions"}],"predecessor-version":[{"id":10653,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/posts\/10560\/revisions\/10653"}],"wp:attachment":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/media?parent=10560"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/categories?post=10560"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/tags?post=10560"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}