Proof Abstraction for Imperative Languages

DOI10.1007/11924661_6MaRDI QIDQ5385589zbMATH OpenOpenAlexFDO

Authors William L. Harrison

Publication date 6 May 2008

Published in Programming Languages and Systems (Search for Journal in Brave)

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

zbMATH Keywords

Language SemanticsMonad TransformersMonadsProgram Specification and Verification

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1231580
• Modular monadic meta-theory
• Separation logic and abstraction
• Modules, abstraction, and parametric polymorphism
• scientific article; zbMATH DE number 1231677

Cited in

(7)

• Theories for mechanical proofs of imperative programs
• Abstraction and subsumption in modular verification of C programs
• ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages
• Abstractions of uniform proofs
• scientific article; zbMATH DE number 6315451 (Why is no real title available?)
• A proof-theoretic study of abstract termination principles
• Modular monadic meta-theory

This page was built for publication: Proof Abstraction for Imperative Languages

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