Mechanized semantics

DOI10.3233/978-1-60750-100-8-195zbMath1213.68206arXiv1010.5582OpenAlexW3037420009MaRDI QIDQ3060983

Xavier Leroy

Publication date: 13 December 2010

Full work available at URL: https://arxiv.org/abs/1010.5582

zbMATH Keywords

operational semanticsdenotational semanticsHoare logicaxiomatic semanticsCoq proof assistantgeneration of verification conditions

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Towards substructural property-based testing ⋮ Proving correctness of a compiler using step-indexed logical relations

Uses Software

• Coq

This page was built for publication: Mechanized semantics