Eliminating Proofs from Programs

F. van Raamsdonk, P. Severi

Research output: Contribution to JournalArticleAcademicpeer-review


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 →
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2002

Bibliographical note

Proceedings title: Porceedings of the International Workshop on Logical Frameworks and Meta-Languages (LFM 2002)
Publisher: Elsevier


Dive into the research topics of 'Eliminating Proofs from Programs'. Together they form a unique fingerprint.

Cite this