A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++

DOI10.1007/S00224-007-9062-1zbMath1166.68009OpenAlexW2017076981MaRDI QIDQ1015388

Ulrich Berger, Rose H. Abdul Rauf, 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

inheritancedenotational semanticsobject-oriented programmingfunctional programmingsimply typed lambda-calculuscorrectness proofKripke-style logical relation

Mathematics Subject Classification ID

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

Uses Software

• Featherweight Java

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• LCF considered as a programming language
• Logical relations and the typed λ-calculus
• Intensional interpretations of functionals of finite type I

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