Dear Colleagues, Please find below some more details about the mini-course on theorem provers for programming language design and specification.
Times and rooms:
- Monday, 11th May, 10:30-12:30 and 14:00-16:00 in room 554, Huxley
- Tuesday, 12th May, 10:30-12:30 and 14:00-16:00 in room 145, Huxley
- Wednesday, 13th May, 10:30-12:30 and 14:00-16:00 in room 554, Huxley
Contents
Program semantics and machine-assisted proofs Programming language semantics is an important topic in computer science, because the semantics guides our understanding of programming. Semantics can be described in a variety of ways; for example, describing the operations of language constructs or describing what the constructs accomplish. The formalization of semantics has in recent years become both feasible and popular to do with mechanical proof assistants, where theorems about a semantics are proved at a higher level of rigor than in corresponding hand proofs and where the machine can assist in producing the proofs in the first place. Proof assistants also come in a variety of flavors; for example, assistants use a variety of logics and provide varying degrees of automation. This makes a difference because the user’s interaction facilities with the tool also shape and color the user’s thinking.
In this intense mini-course, we will study different ways of describing the semantics of a small imperative language. The semantics considered will primarily be a big-step operational semantics, a small-step operational semantics, and a big-step co-inductive semantics. We will also define what correct compilation means and will define a simple compiler that will be proved to be correct. To get some feeling for how these tasks are accomplished using different proof assistants, we will use more than one tool out of: Isabelle/HOL, Coq, F*, and Dafny (final tool selection to be decided).
The course will consist of 12 hours of lectures spread over 3 consecutive days starting May 11. Course participants are expected to, with instruction, do formalization and proofs using the tools (so bring a computer!). There will be homework.
Short Bio:
K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research and Visiting Professor in the Department of Computing at Imperial College London. His research interests include a focus on programming tools, both mental and mechanical. More at http://research.microsoft.com/en-us/um/people/leino/