The correctness of a code generator for a functional language

DOI10.1007/978-3-030-39322-9_4OpenAlexW2998866949MaRDI QIDQ784113FDOQ784113

Authors: Nathanaël Courant, Antoine Séré, Natarajan Shankar 

Publication date: 5 August 2020

Full work available at URL: https://zenodo.org/record/3965629

Recommendations

• scientific article; zbMATH DE number 3947602
• Provably correct code generation: a case study
• Generation of correctness conditions for imperative programs
• Using rewriting techniques to produce code generators and proving them correct
• Sound and complete verification condition generator for functional recursive programs
• A verified compiler for an impure functional language
• scientific article; zbMATH DE number 2079040
• A provably correct compilation of functional languages into scripting languages
• A language-based approach to functionally correct imperative programming
• scientific article; zbMATH DE number 4113956

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

This page was built for publication: The correctness of a code generator for a functional language

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