Functional Programming in Coq

Fall 2019

Course Description:

This course introduces Coq as a functional programming language and as a proof assistant. Some basic concepts and techniques in programming languages and their formal logical underpinnings are also introduced. They will be specified and relevant properties formally verified in Coq. The topics include operational techniques for defining language features, type systems, type safety properties, polymorphism and subtyping.

Instructor	Yuxin Deng
Office	Room B1115, Science Building
Office Hour	10am - 2pm, Monday - Friday
Phone	021-62231281
E-mail	yxdeng(AT)sei.ecnu.edu.cn
Homepage	basics.sjtu.edu.cn/~yuxin/

Reading Materials

Course introduction and the lambda calculus here
The Coq proof assistant. http://coq.inria.fr
Benjamin C. Pierce et al. Software Foundations. https://softwarefoundations.cis.upenn.edu
Yves Bertot, Pierre Casteran. Coq'Art: The Calculus of Inductive Constructions. Springer-Verlag, 2004.

Topics:

Introduction to functional programming
The lambda calculus
Constructive logic
Inductive definitions and proof technique
Formal proofs in Coq
Operational semantics
Formal specificaiton of the WHILE language
Type safety
Subtyping

Grading:

Class participation and discussion: 20%
Homework: 30%
Final exam: 50%

Back