{"id":2742,"date":"2025-10-14T16:19:04","date_gmt":"2025-10-15T01:19:04","guid":{"rendered":"http:\/\/prg.is.titech.ac.jp\/?page_id=2742"},"modified":"2025-10-14T08:00:52","modified_gmt":"2025-10-14T17:00:52","slug":"dependently-typed-music","status":"publish","type":"page","link":"https:\/\/prg.is.titech.ac.jp\/ja\/projects\/formalization\/dependently-typed-music\/","title":{"rendered":"\u4f9d\u5b58\u578b\u4ed8\u304d\u97f3\u697d"},"content":{"rendered":"<p>\u53e2\u60a0\u60a0\" target=\"_blank\" rel=\"noopener\">Youyou Cong<\/a><\/span><\/li>\r\n<li><span style=\"font-size: medium;\">John Leo (Google Seattle)<\/span><\/li>\r\n<\/ul>\r\n<\/div>\r\n<p>\u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0\u8a00\u8a9e\u3067\u306f\u3001\u610f\u5473\u3092\u306a\u3059\u30d7\u30ed\u30b0\u30e9\u30e0\u3092\u66f8\u304f\u305f\u3081\u306b\u578b\u898f\u5247\u3092\u7528\u3044\u307e\u3059\u3002\u4e00\u65b9\u3001\u97f3\u697d\u7406\u8ad6\u3067\u306f\u3001\u97ff\u304d\u306e\u826f\u3044\u97f3\u697d\u3092\u4f5c\u308b\u305f\u3081\u306b\u4f5c\u66f2\u898f\u5247\u3092\u7528\u3044\u307e\u3059\u3002\u3053\u306e\u5bfe\u5fdc\u95a2\u4fc2\u304b\u3089\u3001\u578b\u4ed8\u304d\u97f3\u697d\u306e\u751f\u6210\u3068\u3044\u3046\u767a\u60f3\u304c\u751f\u307e\u308c\u307e\u3059\u3002\u3064\u307e\u308a\u3001\u97f3\u697d\u306e\u898f\u5247\u3092\u578b\u898f\u5247\u3068\u3057\u3066\u8868\u73fe\u3057\u3001\u898f\u5247\u306e\u9055\u53cd\u3092\u578b\u30a8\u30e9\u30fc\u3068\u3057\u3066\u5831\u544a\u3059\u308b\u3001\u3068\u3044\u3046\u8003\u3048\u65b9\u3067\u3059\u3002<\/p>\r\n<p>\u3053\u306e\u30d7\u30ed\u30b8\u30a7\u30af\u30c8\u3067\u306f\u3001\u97f3\u697d\u751f\u6210\u306e\u305f\u3081\u306e\u30e9\u30a4\u30d6\u30e9\u30ea <a href=\"https:\/\/github.com\/halfaya\/MusicTools\/\">Music Tools<\/a> \u3092\u3001Agda \u8a00\u8a9e\u3067\u5b9f\u88c5\u3057\u307e\u3059\u3002\u30a2\u30a4\u30c7\u30a3\u30a2\u3068\u3057\u3066\u306f\u3001Agda \u306e\u4f9d\u5b58\u578b\u3092\u7528\u3044\u3066\u3055\u307e\u3056\u307e\u306a\u4f5c\u66f2\u898f\u5247\u3092\u7c21\u6f54\u306b\u8868\u73fe\u3057\u3064\u3064\u3001FFI \u3092\u901a\u3057\u3066 Haskell \u306e\u97f3\u697d\u751f\u6210\u6a5f\u80fd\u3092\u5229\u7528\u3057\u307e\u3059\u3002<\/p>\r\n<h2><b>\u30e1\u30f3\u30d0\u30fc<\/b><\/h2>\r\n<div>\r\n<ul>\r\n<li><span style=\"font-size: medium;\"><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/cong\/\" data-internallinksmanager029f6b8e52c=\"298\" title=\"\u53e2\u60a0\u60a0\" target=\"_blank\" rel=\"noopener\">\u53e2<\/a> \u60a0\u60a0<\/span><\/li>\r\n<li><span style=\"font-size: medium;\">John Leo (Google Seattle)<\/span><\/li>\r\n<\/ul>\r\n<\/div>\r\n<p><\/p>\r\n\r\n<h2 class=\"wp-block-heading\">\u304a\u77e5\u3089\u305b<\/h2>\r\n\r\n\r\n\r\n<ul class=\"display-posts-listing\"><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/paper-on-continuations-in-music-accepted-to-olivierfest\/\">\u97f3\u697d\u306e\u4e2d\u306e\u7d99\u7d9a\u306b\u95a2\u3059\u308b\u8ad6\u6587\u304c OlivierFest \u306b\u63a1\u629e<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/two-talks-accepted-to-scala-workshop-and-hatra\/\">Scala Workshop \u3068 HATRA \u306b2\u4ef6\u306e\u767a\u8868\u304c\u63a1\u629e<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/paper-on-musical-type-system-farm-2023\/\">\u97f3\u697d\u306e\u305f\u3081\u306e\u578b\u30b7\u30b9\u30c6\u30e0\u306b\u95a2\u3059\u308b\u8ad6\u6587 (@ FARM 2023)<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/tokyo-tech-challenging-research-award\/\">\u53e2\u304c\u6771\u5de5\u5927\u6311\u6226\u7684\u7814\u7a76\u8cde\u3092\u53d7\u8cde<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/lenls-19\/\">\u30d5\u30a1\u30b8\u30a3\u306a\u6027\u8cea\u3092\u8868\u73fe\u3059\u308b\u305f\u3081\u306e\u578b\u7406\u8ad6\u306b\u95a2\u3059\u308b\u767a\u8868 (@ LENLS 19)<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/invited-talk-on-type-theoretic-music-composition-types-2022\/\">\u578b\u7406\u8ad6\u306b\u57fa\u3065\u3044\u305f\u97f3\u697d\u81ea\u52d5\u751f\u6210\u306b\u95a2\u3059\u308b\u62db\u5f85\u8b1b\u6f14  (@ TYPES 2022)<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/talk-on-type-directed-music-composition-yow-lambda-jam-2022\/\">\u578b\u4e3b\u5c0e\u306e\u97f3\u697d\u81ea\u52d5\u751f\u6210\u306b\u95a2\u3059\u308b\u8b1b\u6f14  (@ YOW! Lambda Jam 2022)<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/presentation-on-type-based-music-composition-tfpie-2022\/\">\u578b\u306b\u3088\u308b\u97f3\u697d\u81ea\u52d5\u751f\u6210\u306b\u95a2\u3059\u308b\u767a\u8868  (@ TFPIE 2022)<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/best-poster-award-ppl-2022\/\">\u53e2\u304cPPL 2022\u30dd\u30b9\u30bf\u30fc\u8cde\u3092\u53d7\u8cde<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/presentation-on-type-based-music-generation-at-mus133\/\">\u578b\u30d9\u30fc\u30b9\u306e\u97f3\u697d\u81ea\u52d5\u751f\u6210\u306b\u95a2\u3059\u308b\u767a\u8868(@MUS133)<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/best-poster-award-at-ppl-2021\/\">PPL 2021 \u306b\u304a\u3051\u308b\u30dd\u30b9\u30bf\u30fc\u8cde\u53d7\u8cde<\/a><\/li><li class=\"listing-item\"><a class=\"title\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/poster-demo-presentation-at-ppl2020\/\">PPL2020\u3067\u306e\u30dd\u30b9\u30bf\u30fc\u3068\u30c7\u30e2\u767a\u8868<\/a><\/li><\/ul>","protected":false},"excerpt":{"rendered":"<p>\u53e2\u60a0\u60a0&#8221; target=&#8221;_blank&#8221; rel=&#8221;noopener&#8221;>Youyou Cong John Leo (Google Seattle) \u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0\u8a00\u8a9e\u3067\u306f\u3001\u610f\u5473\u3092\u306a\u3059\u30d7\u30ed\u30b0\u30e9\u30e0\u3092\u66f8\u304f\u305f\u3081\u306b\u578b\u898f\u5247\u3092\u7528\u3044\u307e\u3059&hellip; <a class=\"continue\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/news\/poster-demo-presentation-at-ppl2020\/\">Continue Reading PPL2020\u3067\u306e\u30dd\u30b9\u30bf\u30fc\u3068\u30c7\u30e2\u767a\u8868<\/a><\/p>\n","protected":false},"author":6,"featured_media":0,"parent":8561,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"nf_dc_page":"","footnotes":""},"class_list":["post-2742","page","type-page","status-publish","hentry","radius"],"jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/2742","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/types\/page"}],"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=2742"}],"version-history":[{"count":83,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/2742\/revisions"}],"predecessor-version":[{"id":11213,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/2742\/revisions\/11213"}],"up":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/8561"}],"wp:attachment":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/media?parent=2742"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}