Skip to main content
CSIRO Logo Data 61 logo

Interactive proof: Applications to semantics

Authors

Gerwin Klein

NICTA

UNSW

Abstract

Building on a previous lecture in the summer school, the introduction to interactive proof, this lecture demonstrates a specific application of interactive proof assistants: the semantics of programming languages. In particular, I show how to formalise a small imperative programming language in the theorem prover Isabelle/HOL, how to define its semantics in different variations, and how to prove properties about the language in the theorem prover. The emphasis of the lecture is not on formalising a complex language deeply, but to teach formalisation techniques and proof strategies using simple examples. To this purpose, we cover big- and small step semantics, typing and type safety, as well as a small machine language with compiler and compiler correctness proof.

BibTeX Entry

  @inbook{Klein_12,
    author           = {Klein, Gerwin},
    editor           = {{T. Nipkow, O. Grumberg, B. Hauptmann, G. Kalus}},
    month            = apr,
    series           = {NATO Science for Peace and Security Series},
    year             = {2012},
    keywords         = {isabelle, semantics},
    title            = {Interactive Proof: Applications to Semantics},
    pages            = {85--125},
    booktitle        = {Software Safety and Security: Tools for Analysis and Verification},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/5371.pdf},
    publisher        = {IOS Press},
    isbn             = {978-1-61499-027-7}
  }

Download