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.

基于新颖的观察，即每种编译器中间语言都可以表示为直觉命题逻辑的证明系统，并且这些语言之间的转换与证明转换相对应，这项研究表明，功能语言的编译过程表明，通过自然推论系统的组成和代表的构图，代表了一种拟议的构图，代表了一种构造的构图，并且代表了一种代表的变化，并且从这种证明转换的存在的元级证明中提取。

项目成果

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;篠埜功,大堀淳;上野雄大,大堀淳
• 通讯作者: 上野雄大,大堀淳

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

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

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

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

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

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

Making standard ML a practical database programming language

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

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

宣言的記述からの関数型言語によるゲームプログラムの導出

使用函数式语言从声明性描述中推导游戏程序

• 发表时间: 2011
• 作者: 松島勇介,上野雄大,森畑明昌,大堀淳