Theorem-proving support in programming language semantics

MaRDI QIDQ3400636zbMATH OpenFDO

Authors Yves Bertot

Publication date 5 February 2010

zbMATH Keywords

Coq theorem proverprogramming language semantics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Recommendations

• Encoding natural semantics in Coq
• Mechanized semantics
• Structural Abstract Interpretation: A Formal Study Using Coq
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Formal metatheory of programming languages in the Matita interactive theorem prover

Cited in

(13)

• Winskel is (almost) right: Towards a mechanized semantics textbook
• The Lean 4 theorem prover and programming language
• Teaching semantics with a proof assistant: no more LSD trip proofs
• Proof assistants for natural language semantics
• Lem: a lightweight tool for heavyweight semantics
• Verification conditions for source-level imperative programs
• scientific article; zbMATH DE number 1424019 (Why is no real title available?)
• Formal component-based semantics
• A proof system for MSVL programs in Coq
• Structural Abstract Interpretation: A Formal Study Using Coq
• Jinja: towards a comprehensive formal semantics for a Java-like language
• Typed Lambda Calculi and Applications
• A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming

Describes a project that uses

Uses Software

• Coq
• LOOP

This page was built for publication: Theorem-proving support in programming language semantics

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