Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 index
This course study interactive proof assistants based on higher-order
type theory, and more specifically the Coq system. It studies
generalised inductive definitions (theory and practice). It presents
application of the Coq proof assistant to proof of programs and covers
both functional and imperative programs.
With each course, there will be a practical session on computers.
The evaluation is done with a written exam and optionally a project. The final score is the max of the exam score and the average of the exam and project.
Subject of the project 2010/11 (pdf)
The project should be done individually using the Coq proof assistant.
We request the Coq source file with comments and a small report (max 5 pages). There will be a defense.