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

DOI10.1017/S0956796823000084MaRDI QIDQ6065511zbMATH OpenOpenAlexFDO

Authors Wouter Swierstra

Publication date 11 December 2023

Published in Journal of Functional Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/s0956796823000084

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites work

• \(\lambda\) to SKI, semantically -- declarative pearl
• Advanced Functional Programming
• Another algorithm for bracket abstraction
• Applicative programming with effects
• Dependently typed programming in Agda
• Everybody's got to be somewhere
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(2)

• Axioms for the Theory of Lambda-Conversion
• On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic

This page was built for publication: A correct-by-construction conversion from lambda calculus to combinatory logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6065511)