A Study on Proof-Theoretical Foundations for Compiler Construction

编译器构造的证明理论基础研究

• 批准号: 22500023
• 负责人: OHORI Atsushi
• 金额: $ 2.41万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22500023/
• 关键词: コンパイラ; 証明論; 最適化; プログラミング言語処理系

Based on the novel observations that each of compiler intermediate languages can be represented as a proof system of the intuitionistic propositional logic, and that transformation between these languages corresponds to proof transformation, this research has shown that a compilation process of a functional language is represented by the composition of proof transformations from the natural deduction proof system to a variant of a sequent calculus that represents a code language, and that a compilation algorithm is mechanically extracted from the meta-level proof of the existence of such a proof transformation.

基于每一种编译器中间语言都可以表示为直觉命题逻辑的一个证明系统，并且这些语言之间的转换对应于证明转换的新颖观察，这项研究表明，函数式语言的编译过程是由从自然演绎证明系统到一个表示代码语言，并且编译算法是从元级证明中机械地提取这种证明变换的存在。

项目成果

Rubyの操作的意味論の形式的定義に向けて

走向 Ruby 操作语义的正式定义

• 发表时间: 2013
• 作者: Haruhiko Sato;Masahito Kurihara;高橋俊彦;深澤優鷹,上野雄大,森畑明昌,大堀淳
• 通讯作者: 深澤優鷹,上野雄大,森畑明昌,大堀淳

Design and Implementation of Lightweight First-class Overloading

轻量级重载的设计与实现

• DOI: 10.11309/jssst.29.1_191
• 发表时间: 2012
• 期刊: Computer Software
• 作者: Yusuke Nishimura;Kosuke Maebara;Tomoya Noro;and Takehiro Tokuda;Yusuke Nishimura;篠埜功,大堀淳;上野雄大,大堀淳
• 通讯作者: 上野雄大,大堀淳

Making standard ML a practical database programming language

使标准机器学习成为实用的数据库编程语言

• 发表时间: 2011
• 作者: Atsushi Ohori;Katsuhiro Ueno
• 通讯作者: Katsuhiro Ueno

velopment of SML￥#-making ML an ordinary practical language

SML的发展￥——让ML成为普通的实用语言

• 发表时间: 2011
• 作者: Atsushi Ohori

SML#のSQL統合へのgroupbyの導入

将 groupby 引入 SML 中的 SQL 集成

• 发表时间: 2013
• 作者: 小堀一雄;石居達也;松下誠;井上克郎;斎藤皓,上野雄大,森畑明昌,大堀淳
• 通讯作者: 斎藤皓,上野雄大,森畑明昌,大堀淳