{"created":"2023-05-15T08:55:57.366748+00:00","id":1199,"links":{},"metadata":{"_buckets":{"deposit":"4551960f-bc5b-4c13-97da-d77cc6be112f"},"_deposit":{"created_by":10,"id":"1199","owners":[10],"pid":{"revision_id":0,"type":"depid","value":"1199"},"status":"published"},"_oai":{"id":"oai:tsurumi-u.repo.nii.ac.jp:00001199","sets":["100:101:102:176"]},"author_link":["552"],"item_10007_date_8":{"attribute_name":"報告年度","attribute_value_mlt":[{"subitem_date_issued_datetime":"2016-03-31","subitem_date_issued_type":"Issued"}]},"item_10007_description_13":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"研究成果の概要（和文）：定理証明支援系Coqから，プログラミング言語Scalaへのコード抽出を実現した．Coqによって，コードが正しく動作することの証明を記述した上でコード抽出をすれば，抽出されたコードの正しさが保証される．Scalaコードは，Javaで記述された多数のシステムと親和性が高いと期待される．コード抽出を行うコード自体もCoqで記述されており，その動作が妥当であることが，Coq上の証明として与えられている．","subitem_description_language":"ja","subitem_description_type":"Abstract"},{"subitem_description":"研究成果の概要（英文）：We have implemented code extraction from proof assistant Coq to programming language Scala. Once a proof is given to a code written in Coq, then the extracted code is guaranteed that it behaves correctly. There are many working systems written in Java, and Scala code is easily integrated with them because it runs on Java VM. Our code itself is originally written in Coq and is extracted from a proof on Coq that it works correctly.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_10007_description_14":{"attribute_name":"内容記述","attribute_value_mlt":[{"subitem_description":"・2015(平成27)年度 科学研究費補助金 基盤研究(C) 研究成果報告書","subitem_description_language":"ja","subitem_description_type":"Other"},{"subitem_description":"・研究期間 (年度)：2013-04-01 – 2016-03-31","subitem_description_language":"ja","subitem_description_type":"Other"},{"subitem_description":"・研究分野：情報理工学","subitem_description_language":"ja","subitem_description_type":"Other"}]},"item_10007_description_9":{"attribute_name":"研究課題番号","attribute_value_mlt":[{"subitem_description":"研究課題/領域番号 : 25330096","subitem_description_language":"ja","subitem_description_type":"Other"}]},"item_10007_relation_17":{"attribute_name":"関連サイト","attribute_value_mlt":[{"subitem_relation_type_id":{"subitem_relation_type_id_text":"https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-25330096/","subitem_relation_type_select":"URI"}}]},"item_10007_version_type_20":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_ab4af688f83e57aa","subitem_version_type":"AM"}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2022-04-20"}],"displaytype":"detail","filename":"25330096.pdf","filesize":[{"value":"264.6 kB"}],"format":"application/pdf","licensetype":"license_6","mimetype":"application/pdf","url":{"label":"25330096","url":"https://tsurumi-u.repo.nii.ac.jp/record/1199/files/25330096.pdf"},"version_id":"c2105482-b4ed-4739-bf8b-e31682a3ce91"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"定理証明支援系","subitem_subject_language":"ja","subitem_subject_scheme":"Other"},{"subitem_subject":"ソフトウェア検証","subitem_subject_language":"ja","subitem_subject_scheme":"Other"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_researcher":{"attribute_name":"研究代表者","attribute_type":"creator","attribute_value_mlt":[{"creatorAffiliations":[{"affiliationNameIdentifiers":[{"affiliationNameIdentifier":"","affiliationNameIdentifierScheme":"ISNI","affiliationNameIdentifierURI":"http://www.isni.org/isni/"}],"affiliationNames":[{"affiliationName":"","affiliationNameLang":"ja"}]}],"creatorNames":[{"creatorName":"TANABE, Yoshinori","creatorNameLang":"en"},{"creatorName":"田辺, 良則","creatorNameLang":"ja"},{"creatorName":"タナベ, ヨシノリ","creatorNameLang":"ja-Kana"}],"familyNames":[{"familyName":"TANABE","familyNameLang":"en"},{"familyName":"田辺","familyNameLang":"ja"},{"familyName":"タナベ","familyNameLang":"ja-Kana"}],"givenNames":[{"givenName":"Yoshinori","givenNameLang":"en"},{"givenName":"良則","givenNameLang":"ja"},{"givenName":"ヨシノリ","givenNameLang":"ja-Kana"}],"nameIdentifiers":[{"nameIdentifier":"552","nameIdentifierScheme":"WEKO"},{"nameIdentifier":"60443199","nameIdentifierScheme":"e-Rad","nameIdentifierURI":"https://kaken.nii.ac.jp/ja/search/?qm=60443199"},{"nameIdentifier":"552","nameIdentifierScheme":"WEKO著者ID"}]}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"research report","resourceuri":"http://purl.org/coar/resource_type/c_18ws"}]},"item_title":"定理証明器によるモジュラーなソフトウェア検証","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"定理証明器によるモジュラーなソフトウェア検証","subitem_title_language":"ja"},{"subitem_title":"Modular software verification with a proof assistant","subitem_title_language":"en"}]},"item_type_id":"10007","owner":"10","path":["176"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2022-04-20"},"publish_date":"2022-04-20","publish_status":"0","recid":"1199","relation_version_is_last":true,"title":["定理証明器によるモジュラーなソフトウェア検証"],"weko_creator_id":"10","weko_shared_id":-1},"updated":"2024-08-01T07:33:26.186895+00:00"}