TY - GEN
T1 - Teaching semantics with a proof assistant
T2 - 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
AU - Nipkow, Tobias
PY - 2012
Y1 - 2012
N2 - We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic. The course is entirely based on the proof assistant Isabelle and includes a compact introduction to Isabelle. The overall aim is to teach the students how to write correct and readable proofs.
AB - We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic. The course is entirely based on the proof assistant Isabelle and includes a compact introduction to Isabelle. The overall aim is to teach the students how to write correct and readable proofs.
UR - http://www.scopus.com/inward/record.url?scp=84856182330&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-27940-9_3
DO - 10.1007/978-3-642-27940-9_3
M3 - Conference contribution
AN - SCOPUS:84856182330
SN - 9783642279393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 24
EP - 38
BT - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
Y2 - 22 January 2012 through 24 January 2012
ER -