A provably correct translation of the -calculus into a mathematical model of C++

DOI10.1007/S00224-007-9062-1MaRDI QIDQ1015388zbMATH OpenOpenAlexFDO

Authors Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer

Publication date 8 May 2009

Published in Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL https://cronfa.swan.ac.uk/Record/cronfa135

zbMATH Keywords

correctness proofdenotational semanticsfunctional programminginheritanceKripke-style logical relationobject-oriented programmingsimply typed lambda-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Notions of computation and monads
• scientific article; zbMATH DE number 1456954
• A provably correct compilation of functional languages into scripting languages
• From a concurrent λ-calculus to the π-calculus
• Functional runtime systems within the lambda-sigma calculus

Cites work

• scientific article; zbMATH DE number 1650458 (Why is no real title available?)
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 3909708 (Why is no real title available?)
• scientific article; zbMATH DE number 512784 (Why is no real title available?)
• scientific article; zbMATH DE number 1948186 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• LCF considered as a programming language
• Logical relations and the typed λ-calculus
• Notions of computation and monads

Cited in

(2)

• A provably correct compilation of functional languages into scripting languages
• Translating lambda calculus into C++ templates

Describes a project that uses

Uses Software

• Featherweight Java

This page was built for publication: A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++

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