Mechanized semantics
From MaRDI portal
Abstract: The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and over generic program transformations, as typically found in compilers. The topics covered include: operational semantics (small-step, big-step, definitional interpreters); a simple form of denotational semantics; axiomatic semantics and Hoare logic; generation of verification conditions, with application to program proof; compilation to virtual machine code and its proof of correctness; an example of an optimizing program transformation (dead code elimination) and its proof of correctness.
Recommendations
- Semantics and program verification
- Computer Science Logic
- Theories for mechanical proofs of imperative programs
- Mechanized verification of computing dominators for formalizing compilers
- scientific article; zbMATH DE number 2079677
- Towards a theory of semantics and compilers for programming languages
- From rewriting logic, to programming language semantics, to program verification
Cited in
(6)- Theories for mechanical proofs of imperative programs
- Proving correctness of a compiler using step-indexed logical relations
- Teaching semantics with a proof assistant: no more LSD trip proofs
- Theorem-proving support in programming language semantics
- Towards a theory of semantics and compilers for programming languages
- Towards substructural property-based testing
This page was built for publication: Mechanized semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3060983)
