From OBJ to ML to Coq

DOI10.1007/11780274_12MaRDI QIDQ5757928zbMATH OpenOpenAlexFDO

Authors Jacek Chrząszcz, Jean-Pierre Jouannaud

Publication date 7 September 2007

Published in Algebra, Meaning, and Computation (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• Specification and verification challenges for sequential object-oriented programs
• Verifying programs in the calculus of inductive constructions
• Modular development of certified program verifiers with a proof assistant,
• Program development in constructive type theory
• Verifying object-oriented programs with higher-order separation logic in Coq

Cited in

(1)

• scientific article; zbMATH DE number 4157861 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: From OBJ to ML to Coq

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