Teaching semantics with a proof assistant: no more LSD trip proofs
DOI10.1007/978-3-642-27940-9_3zbMATH Open1325.68005OpenAlexW2293069733MaRDI QIDQ2891399FDOQ2891399
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
Recommendations
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)
Cites Work
- Automatic proof and disproof in Isabelle/HOL
- A Brief Overview of Mizar
- Nominal techniques in Isabelle/HOL
- Semantics with applications: an appetizer.
- A comparison of Mizar and Isar
- A certified denotational abstract interpreter
- Title not available (Why is that?)
- Winskel is (almost) right: Towards a mechanized semantics textbook
- Programming Languages and Systems
- Title not available (Why is that?)
- Turning Inductive into Equational Specifications
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
Uses Software
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)
