Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis†

DOI10.1017/S0956796800001581zbMath0854.68018OpenAlexW2062274057WikidataQ123332080 ScholiaQ123332080MaRDI QIDQ4880526

Daniel Le Métayer, Geoffrey L. Burn

Publication date: 9 June 1996

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

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

zbMATH Keywords

compilerprogram analyses

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Cites Work

• Two-level semantics and abstract interpretation
• Strictness analysis for higher-order functions
• Two-level semantics and code generation
• The categorical abstract machine
• Strictness analysis and denotational abstract interpretation
• More on advice on structuring compilers and proving them correct
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Program transformations in a denotational setting
• Deriving Target Code as a Representation of Continuation Semantics
• Abstract interpretation and application to logic programs
• Abstract Interpretation Frameworks
• Unnamed Item
• Unnamed Item

This page was built for publication: Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^†