Eliminating Proofs from Programs

F. van Raamsdonk; P. Severi

doi:10.1016/s1571-0661(04)80505-x

Eliminating Proofs from Programs

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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 language	English
Journal	Electronic Notes in Theoretical Computer Science
Volume	70
DOIs	https://doi.org/10.1016/s1571-0661(04)80505-x
Publication status	Published - 2002

Bibliographical note

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

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1016/s1571-0661(04)80505-x

Persistent URL (handle)

Persistent link

Cite this

@article{61d3677c3732437383ab440a57baa78f,

title = "Eliminating Proofs from Programs",

abstract = "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 →",

author = "{van Raamsdonk}, F. and P. Severi",

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

year = "2002",

doi = "10.1016/s1571-0661(04)80505-x",

language = "English",

volume = "70",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Eliminating Proofs from Programs

AU - van Raamsdonk, F.

AU - Severi, P.

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

PY - 2002

Y1 - 2002

N2 - 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 →

AB - 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 →

U2 - 10.1016/s1571-0661(04)80505-x

DO - 10.1016/s1571-0661(04)80505-x

M3 - Article

SN - 1571-0661

VL - 70

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Eliminating Proofs from Programs

Abstract

Bibliographical note

UN SDGs

Access to Document

Persistent URL (handle)

Fingerprint

Cite this