Theorem-proving support in programming language semantics

zbMATH Open1195.68090MaRDI QIDQ3400636FDOQ3400636

Authors: Yves Bertot 

Publication date: 5 February 2010

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

zbMATH Keywords

programming language semanticsCoq theorem prover

Mathematics Subject Classification ID

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

Cited In (12)

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

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)