WEKO3
アイテム
A Type System for Verification of Compiler Optimizations
https://ipsj.ixsq.nii.ac.jp/records/16672
https://ipsj.ixsq.nii.ac.jp/records/166726bad57c3-a5ac-4590-8036-02e69a4cdcff
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO4509003.pdf (253.5 kB)
|
Copyright (c) 2004 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2004-07-15 | |||||||
| タイトル | ||||||||
| タイトル | A Type System for Verification of Compiler Optimizations | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Type System for Verification of Compiler Optimizations | |||||||
| 言語 | ||||||||
| 言語 | eng | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| Department of Frontier Informatics The University of Tokyo | ||||||||
| 著者所属 | ||||||||
| Information Technology Center The University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Frontier Informatics, The University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Information Technology Center, The University of Tokyo | ||||||||
| 著者名 |
YUTAKA, MATSUNO
HIROYUKI, SATO
× YUTAKA, MATSUNO HIROYUKI, SATO
|
|||||||
| 著者名(英) |
Yutaka, Matsuno
Hiroyuki, Sato
× Yutaka, Matsuno Hiroyuki, Sato
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 45, 号 SIG09(PRO22), p. 14-24, 発行日 2004-07-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
