DocumentCode
2258992
Title
Program extraction by type erasing
Author
Zhu, Ming-Yuan ; Ding, Yi-Qiang
Author_Institution
AI Lab., Beijing Inst. of Syst. Eng., China
fYear
1994
fDate
9-11 Nov 1994
Firstpage
105
Lastpage
110
Abstract
PowerEpsilon is a proof development system based on Martin-Lof´s type theory and the calculus of constructions. It contains a logic, a specification language and a programming language, so it is a powerful tool with different uses, However, the constructive type theory is an integrated logic in which the logical and computational parts are associated so well that to extract a program from a proof is not a straightforward task. In this paper, a new approach for extracting program from a proof called type erasing is proposed
Keywords
functional programming; lambda calculus; type theory; PowerEpsilon; calculus of constructions; constructive type theory; integrated logic; program extraction; programming language; proof development system; specification language; type erasing; Artificial intelligence; Calculus; Computer languages; Computer science; Functional programming; Laboratories; Logic programming; Power engineering and energy; Specification languages; Systems engineering and theory;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Software and Applications Conference, 1994. COMPSAC 94. Proceedings., Eighteenth Annual International
Conference_Location
Taipei
Print_ISBN
0-8186-6705-2
Type
conf
DOI
10.1109/CMPSAC.1994.342822
Filename
342822
Link To Document