{"updated":"2025-01-20T17:51:52.104558+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00146691","sets":["6164:6805:6807:8441"]},"path":["8441"],"owner":"10","recid":"146691","title":["Agdaによる型推論器の定式化"],"pubdate":{"attribute_name":"公開日","attribute_value":"2015-01-09"},"_buckets":{"deposit":"6e0376a9-b9ad-45d2-8fe3-d7f9ae50c320"},"_deposit":{"id":"146691","pid":{"type":"depid","value":"146691","revision_id":0},"owners":[10],"status":"published","created_by":10},"item_title":"Agdaによる型推論器の定式化","author_link":["229753","229752","229751","229754"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Agdaによる型推論器の定式化"},{"subitem_title":"Type Inference in Agda","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"Agda, Type Inference, Proof Theory","subitem_subject_scheme":"Other"}]},"item_type_id":"18","publish_date":"2015-01-09","item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_18_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"お茶の水女子大学"},{"subitem_text_value":"お茶の水女子大学"}]},"item_18_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Ochanomizu University","subitem_text_language":"en"},{"subitem_text_value":"Ochanomizu University","subitem_text_language":"en"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/146691/files/IPSJ-WPRO2015020.pdf","label":"IPSJ-WPRO2015020.pdf"},"date":[{"dateType":"Available","dateValue":"2015-01-09"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-WPRO2015020.pdf","filesize":[{"value":"270.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"be0315a2-10db-4d96-8751-11de6fd38f16","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2015 by the Information Processing Society of Japan"}]},"item_18_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"門脇, 香子"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"浅井, 健一"}],"nameIdentifiers":[{}]}]},"item_18_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Kyoko, Kadowaki","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Kenichi, Asai","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_5794","resourcetype":"conference paper"}]},"item_18_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"Agda はマルティンレフの型理論に基づいた定理証明支援器であり,その一方で依存型をもつ関数型プログラミング言語でもある.Agda では依存型 (Dependant Types) を用いることができるのも大きな特徴である.また,定理証明支援器とプログラミング言語両方の特徴をもちあわせていることから,何かを実装しつつ証明するのに適している.そこで本稿では,停止性が保証された型推論器を Agda により構成する.なかでも, Unification の実装では, McBride の手法を採用する.これは型変数の数を巧妙に管理することで構造に従った再帰を使って(つまり停止性が明らかな形で)型の Unification を表現できることを示したものである.本稿では Term の型変数の数に注目しつつ,主に Unification の部分と Application の実装にフォーカスを当てながら実装していく.","subitem_description_type":"Other"}]},"item_18_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"Agda is a dependently typed functional programming language based on Zhaohui Luo's UTT a type theory similar to Martin-L‡f type theory.  Agda is also based on dependent type theory.This paper used Agda to implement a Type inference guaranteed to avoid compose non-stopping program by a structural recursion of McBride's technique. This paper focused number of typing variables, Unification and implementation of application data constructor.","subitem_description_type":"Other"}]},"item_18_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"120","bibliographic_titles":[{"bibliographic_title":"第56回プログラミング･シンポジウム予稿集"}],"bibliographicPageStart":"115","bibliographicIssueDates":{"bibliographicIssueDate":"2015-01-09","bibliographicIssueDateType":"Issued"},"bibliographicVolumeNumber":"2015"}]},"relation_version_is_last":true,"weko_creator_id":"10"},"created":"2025-01-19T00:22:07.636634+00:00","id":146691,"links":{}}