{"created":"2025-01-18T22:49:52.756432+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00016672","sets":["934:935:959:961"]},"path":["961"],"owner":"1","recid":"16672","title":["A Type System for Verification of Compiler Optimizations"],"pubdate":{"attribute_name":"公開日","attribute_value":"2004-07-15"},"_buckets":{"deposit":"83d1a6d2-2cd2-4118-b4ec-56fde39dd2ae"},"_deposit":{"id":"16672","pid":{"type":"depid","value":"16672","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"A Type System for Verification of Compiler Optimizations","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"A Type System for Verification of Compiler Optimizations"},{"subitem_title":"A Type System for Verification of Compiler Optimizations","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"通常論文","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2004-07-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"Department of Frontier Informatics  The University of Tokyo"},{"subitem_text_value":"Information Technology Center  The University of Tokyo"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Department of Frontier Informatics, The University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"Information Technology Center, The University of Tokyo","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"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/16672/files/IPSJ-TPRO4509003.pdf"},"date":[{"dateType":"Available","dateValue":"2006-07-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO4509003.pdf","filesize":[{"value":"253.5 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"a1d4db98-78a2-43f5-9252-ac4fbe2b7d42","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2004 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"YUTAKA, MATSUNO"},{"creatorName":"HIROYUKI, SATO"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Yutaka, Matsuno","creatorNameLang":"en"},{"creatorName":"Hiroyuki, Sato","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"This paper presents a type theoretical framework for the verification of compiler optimizations. Though today's compiler optimizations are fairly advanced  there is still not an appropriate theoretical framework for the verification of compiler optimizations. To establish a generalized framework  we introduce assignment types for variables  which represent how the value of variables will be calculated in a program. First we introduce our type system. Second we prove soundness of our type system meaning that if types of return values are equal in two programs  the programs are equivalent. Soundness ensures that many structure preserving optimizations preserve program semantics. Then by extending the notion of type equality to order relation  we redefine several optimizations and prove that they also preserve program semantics.","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"This paper presents a type theoretical framework for the verification of compiler optimizations. Though today's compiler optimizations are fairly advanced, there is still not an appropriate theoretical framework for the verification of compiler optimizations. To establish a generalized framework, we introduce assignment types for variables, which represent how the value of variables will be calculated in a program. First we introduce our type system. Second we prove soundness of our type system meaning that if types of return values are equal in two programs, the programs are equivalent. Soundness ensures that many structure preserving optimizations preserve program semantics. Then by extending the notion of type equality to order relation, we redefine several optimizations and prove that they also preserve program semantics.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"24","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"14","bibliographicIssueDates":{"bibliographicIssueDate":"2004-07-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"SIG09(PRO22)","bibliographicVolumeNumber":"45"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"links":{},"id":16672,"updated":"2025-01-22T23:44:26.694726+00:00"}