Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs

DOI10.1007/978-3-642-27940-9_3zbMath1325.68005OpenAlexW2293069733MaRDI QIDQ2891399

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

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

Related Items (3)

A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Semantics with applications: an appetizer.
• Nominal techniques in Isabelle/HOL
• Winskel is (almost) right: Towards a mechanized semantics textbook
• A comparison of Mizar and Isar
• Automatic Proof and Disproof in Isabelle/HOL
• A Brief Overview of Mizar
• Turning Inductive into Equational Specifications
• A Certified Denotational Abstract Interpreter
• Programming Languages and Systems

This page was built for publication: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs