WEKO3
アイテム
{"_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\u0027\u0027 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", "download_preview_message": "", "file_order": 0, "filename": "12-002E.pdf", "filesize": [{"value": "271.1 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 271100.0, "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"], "permalink_uri": "https://doi.org/10.20736/0000001267", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2019-03-13"}, "publish_date": "2019-03-13", "publish_status": "0", "recid": "1267", "relation": {}, "relation_version_is_last": true, "title": ["NII Technical Report (NII-2012-002E):Formalization of Lemma for Adjacent Replacement Paths"], "weko_shared_id": -1}
NII Technical Report (NII-2012-002E):Formalization of Lemma for Adjacent Replacement Paths
https://doi.org/10.20736/0000001267
https://doi.org/10.20736/0000001267e4540fde-5b8a-49f0-9f83-15dc08c9ed2a
名前 / ファイル | ライセンス | アクション |
---|---|---|
NII Technical Report (NII-2012-002E):Formalization of Lemma for Adjacent Replacement Paths (271.1 kB)
|
|
Item type | レポート / Report(1) | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
公開日 | 2019-03-13 | |||||||||
タイトル | ||||||||||
言語 | en | |||||||||
タイトル | NII Technical Report (NII-2012-002E):Formalization of Lemma for Adjacent Replacement Paths | |||||||||
言語 | ||||||||||
言語 | eng | |||||||||
キーワード | ||||||||||
言語 | ja | |||||||||
主題Scheme | Other | |||||||||
主題 | テクニカルレポート | |||||||||
キーワード | ||||||||||
言語 | en | |||||||||
主題Scheme | Other | |||||||||
主題 | Technical Report | |||||||||
資源タイプ | ||||||||||
資源 | http://purl.org/coar/resource_type/c_6501 | |||||||||
タイプ | departmental bulletin paper | |||||||||
ID登録 | ||||||||||
ID登録 | 10.20736/0000001267 | |||||||||
ID登録タイプ | JaLC | |||||||||
著者 |
龍田, 真
× 龍田, 真
|
|||||||||
抄録 | ||||||||||
内容記述タイプ | Abstract | |||||||||
内容記述 | 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. | |||||||||
言語 | en | |||||||||
書誌情報 |
ja : NIIテクニカル・レポート en : NII Technical Report p. 1-25, 発行日 2012-02-17 |
|||||||||
出版者 | ||||||||||
言語 | ja | |||||||||
出版者 | 国立情報学研究所 | |||||||||
ISSN | ||||||||||
収録物識別子タイプ | ISSN | |||||||||
収録物識別子 | 1346-5597 |