Proving the correctness of recursion-based automatic program transformations

DOI10.1007/3-540-59293-8_228zbMath1496.68118OpenAlexW1509231339MaRDI QIDQ5096758

David Sands

Publication date: 18 August 2022

Published in: TAPSOFT '95: Theory and Practice of Software Development (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-59293-8_228

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deforestation: Transforming programs to eliminate trees
• A syntactic theory of sequential control
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• The concept of a supercompiler
• Infinite trees in normal form and recursive equations having a unique solution
• Partial evaluation in logic programming
• A Transformation System for Developing Recursive Programs
• On-line and off-line partial evaluation: semantic specifications and correctness proofs

This page was built for publication: Proving the correctness of recursion-based automatic program transformations