Mechanized operational semantics via (co)induction

DOI10.1007/3-540-48256-3_15MaRDI QIDQ4945209zbMATH OpenFDO

Authors Simon J. Ambler, Roy L. Crole

Publication date 23 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48256-3_15

zbMATH Keywords

automated proofbisimulationcontextual equivalenceprogramming languagetheorem proves Isabelle98

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• Winskel is (almost) right: Towards a mechanized semantics textbook
• A case study in programming coinductive proofs: Howe's method
• Theorem-proving support in programming language semantics
• Encoding natural semantics in Coq
• scientific article; zbMATH DE number 3870631

Cited in

(5)

• Winskel is (almost) right: Towards a mechanized semantics textbook
• \(\mathrm{HO}\pi\) in Coq
• Automating soundness proofs
• A case study in programming coinductive proofs: Howe's method
• Winskel is (almost) right. Towards a mechanized semantics textbook

This page was built for publication: Mechanized operational semantics via (co)induction

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