Algebraic correctness proofs for compiling recursive function definitions with strictness information

DOI10.1007/s00236-006-0013-0zbMath1097.68025OpenAlexW2020799479MaRDI QIDQ2502270

Klaus Indermark, Thomas Noll

Publication date: 12 September 2006

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-006-0013-0

zbMATH Keywords

Formal semanticsFunctional languagesCompiler correctnessEvaluation strategiesStack implementation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Uses Software

• CLEAN
• OBJ3
• Maude

Cites Work

• Least fixed points revisited
• A lattice-theoretical fixpoint theorem and its applications
• Sequential formula translation
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Initial Algebra Semantics and Continuous Algebras
• Fixpoint approach to the theory of computation
• The Mechanical Evaluation of Expressions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Algebraic correctness proofs for compiling recursive function definitions with strictness information