A correct-by-construction conversion from lambda calculus to combinatory logic

Wouter Swierstra

doi:10.1017/S0956796823000084

A correct-by-construction conversion from lambda calculus to combinatory logic

Wouter Swierstra

Sub Software Technology

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

Abstract

This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.

Original language	English
Article number	e11
Pages (from-to)	1-9
Number of pages	9
Journal	Journal of Functional Programming
Volume	33
Issue number	1
DOIs	https://doi.org/10.1017/S0956796823000084
Publication status	Published - 2023

Access to Document

10.1017/S0956796823000084Licence: CC BY

a-correct-by-construction-conversion-from-lambda-calculus-to-combinatory-logicFinal published version, 114 KBLicence: CC BY

Cite this

@article{a890757ad07c40289b9a173a88ddc52e,

title = "A correct-by-construction conversion from lambda calculus to combinatory logic",

abstract = "This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.",

author = "Wouter Swierstra",

year = "2023",

doi = "10.1017/S0956796823000084",

language = "English",

volume = "33",

pages = "1--9",

journal = "Journal of Functional Programming",

issn = "0956-7968",

publisher = "Cambridge University Press",

number = "1",

}

TY - JOUR

T1 - A correct-by-construction conversion from lambda calculus to combinatory logic

AU - Swierstra, Wouter

PY - 2023

Y1 - 2023

N2 - This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.

AB - This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.

UR - http://www.scopus.com/inward/record.url?scp=85179757521&partnerID=8YFLogxK

U2 - 10.1017/S0956796823000084

DO - 10.1017/S0956796823000084

M3 - Article

SN - 0956-7968

VL - 33

SP - 1

EP - 9

JO - Journal of Functional Programming

JF - Journal of Functional Programming

IS - 1

M1 - e11

ER -

A correct-by-construction conversion from lambda calculus to combinatory logic

Abstract

Access to Document

Fingerprint

Cite this