Teaching semantics with a proof assistant: no more LSD trip proofs

DOI10.1007/978-3-642-27940-9_3MaRDI QIDQ2891399zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow

Publication date 15 June 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-27940-9_3

Mathematics Subject Classification ID

Theory of programming languages (68N15) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Semantics in the theory of computing (68Q55) Programming languages (educational aspects) (97P40)

Recommendations

• Concrete semantics. With Isabelle/HOL
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Mechanized semantics
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem-proving support in programming language semantics

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• A Brief Overview of Mizar
• A certified denotational abstract interpreter
• A comparison of Mizar and Isar
• Automatic proof and disproof in Isabelle/HOL
• Nominal techniques in Isabelle/HOL
• Programming Languages and Systems
• Semantics with applications: an appetizer.
• Turning Inductive into Equational Specifications
• Winskel is (almost) right: Towards a mechanized semantics textbook

Cited in

(6)

• Winskel is (almost) right. Towards a mechanized semantics textbook
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Concrete semantics. With Isabelle/HOL
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• SeCaV: a sequent calculus verifier in Isabelle/HOL

Describes a project that uses

Uses Software

• DrACuLa
• Nominal Isabelle
• Sledgehammer
• Mizar
• Isar
• Isabelle/HOL
• DrScheme
• Isabelle
• ACL2

This page was built for publication: Teaching semantics with a proof assistant: no more LSD trip proofs

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