Deriving proof rules from continuation semantics

DOI10.1007/S001650050041MaRDI QIDQ1974480zbMATH OpenOpenAlexFDO

Authors Philippe Audebaud, Elena Zucca

Publication date 7 May 2000

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s001650050041

zbMATH Keywords

continuation style semanticsHoare semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 4058826
• Towards a unified theory of operational and axiomatic semantics
• On the transformation between direct and continuation semantics
• Towards reasoning about Hoare relations
• Logic Based Program Synthesis and Transformation

Cited in

(7)

• scientific article; zbMATH DE number 683357 (Why is no real title available?)
• scientific article; zbMATH DE number 1973223 (Why is no real title available?)
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• scientific article; zbMATH DE number 1497842 (Why is no real title available?)
• Derivability of rules from rule complexes
• Logic Based Program Synthesis and Transformation
• A general proof rule for procedures in predicate transformer semantics

This page was built for publication: Deriving proof rules from continuation semantics

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