MSM

Print

MSM: Mechanized Semantics

Person in charge: Sandrine Blazy (mail)

Pedagogical team: Sandrine Blazy et David Pichardie (mail)

Description

Rigorous justification of a scientific work is an important part in the research activity in Computer Science. This course starts with the observation that some students find it difficult to make themselves a rigourous argumentation, largely because of a lack of practice during their previous studies. The course is intended to recall the basic elements to achieve a rigorous proof and a personal tutorship for the student to realize his own work. The course is based on two case studies in Computer Science.

  • Proof assistants: proofs can be done inside a tool like Coq (http://coq.inria.fr). The tool is in charge of verifying the correctness of each elementary proof step. The course is not about Coq itself. Only a few features of the tool will be presented. The goal is to allow the student to use the tool during is personal project. Lectures will be given using the tool and students will be encouraged to use it during the lectures.
  • Semantics: a formal language semantics allows to describe unambiguously the expected behavior of programs. It is for example possible to establish the correctness of a compiler by proving that a source program and a target program share the same observable behaviors with respect to their semantics. The course will take some semantics as object of study: various form of semantics, for various language features (imperative, object, concurrent).

The lecture will follow some parts of the online book Software Foundations by Pierce et al.. Students will be given some reading to complete the lectures.

The lecture will end with a presentation of some recent research about a formal semantics of C in Coq (cf http://compcert.inria.fr).

Keywords: machine checked proofs, programming language semantics

Prerequisites: basic notions of functional programming, compilers and logic

Learning outcomes

  • Writing a proof that is both rigorous and correct.
  • Basic skills in using a proof assistant
  • Rigorous description of the expected behavior of a program
  • Meta-theoretic study of various programming language features

Contents

  • Discovering the Coq proof assistant
  • Reasoning by induction on integers and lists
  • Modeling of a little programming language: syntax and semantics
  • Proofs of semantics properties
  • Verification of a little compiler

The course unit is composed of 14h of lectures and 6h of support for the students personal project.

Bibliography

  • Nielson H.R., Nielson F. Semantics with applications: A formal introduction. Wiley, 1992
  • Pierce B.C. Software Foundations. http://www.cis.upenn.edu/~bcpierce/sf/

Evaluation mode

  • homework (20%) + 1 personal project (40%) + 1 final exam (40%)
Buy cheap web hosting service where fatcow web hosting review will give you advices and please read bluehost review for more hosting information.