![]() ![]() |
|
タケヤマ マコト
Takeyama Makoto 武山 誠 所属 神奈川大学 理学部 情報科学科 神奈川大学大学院 理学研究科 理学専攻(情報科学領域) 職種 教授 |
|
言語種別 | 英語 |
発行・発表の年月 | 2005 |
形態種別 | その他論文 |
査読 | 査読あり |
標題 | An Emacs Interaface for Type-Directed Support for Constructing Proofs and Programs |
執筆形態 | 共著 |
掲載誌名 | User Interfaces for Theorem Provers UITP 2005 |
掲載区分 | 国外 |
著者・共著者 | Catarina Coquand, Dan Synek, Makoto Takeyama |
概要 | This paper presents an emacs interface for an interactive editor for proofs and programs. The interface allows for editing proofs in the same way as we write programs, but in addition offers commands that help term construction. It differs from most other proof editors for its support for direct construction of terms rather than tactics for building them. |