Title :
Program extraction by type erasing
Author :
Zhu, Ming-Yuan ; Ding, Yi-Qiang
Author_Institution :
AI Lab., Beijing Inst. of Syst. Eng., China
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;
Conference_Titel :
Computer Software and Applications Conference, 1994. COMPSAC 94. Proceedings., Eighteenth Annual International
Conference_Location :
Taipei
Print_ISBN :
0-8186-6705-2
DOI :
10.1109/CMPSAC.1994.342822
