Sciweavers

ENTCS
2002

Eliminating Proofs from Programs

13 years 9 months ago
Eliminating Proofs from Programs
This paper presents a step in the development of an operational approach to program extraction in type theory. In order to get a program from a lambda term, the logical parts need to be removed. This is done by a reduction relation . We study the combination of -reduction and -reduction, both in the setting of simply typed lambda calculus and for pure type systems. In the general setting the properties confluence, subject reduction, and strong normalization are studied.
Femke van Raamsdonk, Paula Severi
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Where ENTCS
Authors Femke van Raamsdonk, Paula Severi
Comments (0)