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

DOI10.1007/978-3-642-27940-9_3zbMath1325.68005MaRDI 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

68-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science

68N15: Theory of programming languages

68Q55: Semantics in the theory of computing

97P40: Programming languages (educational aspects)

Uses Software

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