Functional Programming in Coq

Fall 2017

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.

InstructorYuxin 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



Topics:



Grading:



Back