{"created":"2021-03-01T05:52:58.957916+00:00","id":1267,"links":{},"metadata":{"_buckets":{"deposit":"3b187ec0-ace5-4d43-ad5e-33c7fbc0629f"},"_deposit":{"id":"1267","owners":[],"pid":{"revision_id":0,"type":"depid","value":"1267"},"status":"published"},"_oai":{"id":"oai:repository.nii.ac.jp:00001267","sets":["136"]},"author_link":[],"control_number":"1267","item_5_biblio_info_30":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2012-02-17","bibliographicIssueDateType":"Issued"},"bibliographicPageEnd":"25","bibliographicPageStart":"1","bibliographic_titles":[{"bibliographic_title":"NIIテクニカル・レポート","bibliographic_titleLang":"ja"},{"bibliographic_title":"NII Technical Report","bibliographic_titleLang":"en"}]}]},"item_5_description_28":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"This paper formalizes the proof of Lemma A13 given in the paper ``Compositional characterizations of lambda-terms using intersection types'' by M.~Dezani-Ciancaglini et al, so that one can verify it by a theorem prover such as HOL by typing the content of this paper. The proof in the original paper is simplified by reorganizing case analysis. Several properties implicitly used in the original paper are explicitly stated and proved.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_5_identifier_registration":{"attribute_name":"ID登録","attribute_value_mlt":[{"subitem_identifier_reg_text":"10.20736/0000001267","subitem_identifier_reg_type":"JaLC"}]},"item_5_publisher_31":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"国立情報学研究所","subitem_publisher_language":"ja"}]},"item_5_source_id_32":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1346-5597","subitem_source_identifier_type":"ISSN"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"龍田, 真","creatorNameLang":"ja"},{"creatorName":"Tatsuta, Makoto","creatorNameLang":"en"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2019-03-13"}],"displaytype":"detail","filename":"12-002E.pdf","filesize":[{"value":"271.1 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"NII Technical Report (NII-2012-002E)：Formalization of Lemma for Adjacent Replacement Paths","url":"https://repository.nii.ac.jp/record/1267/files/12-002E.pdf"},"version_id":"6d6aa7b1-30b9-4894-82a5-6cfce1a126d3"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"テクニカルレポート","subitem_subject_language":"ja","subitem_subject_scheme":"Other"},{"subitem_subject":"Technical Report","subitem_subject_language":"en","subitem_subject_scheme":"Other"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"departmental bulletin paper","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"NII Technical Report (NII-2012-002E)：Formalization of Lemma for Adjacent Replacement Paths","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"NII Technical Report (NII-2012-002E)：Formalization of Lemma for Adjacent Replacement Paths","subitem_title_language":"en"}]},"item_type_id":"5","owner":"1","path":["136"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2019-03-13"},"publish_date":"2019-03-13","publish_status":"0","recid":"1267","relation_version_is_last":true,"title":["NII Technical Report (NII-2012-002E)：Formalization of Lemma for Adjacent Replacement Paths"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-11T02:10:17.107504+00:00"}