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
logical verification 2006 - 2007
logical verification 2006 - 2007
Contents of the course
A proof-assistant is used to check the correctness of
a specification of a program, or the proof of a theorem.
In the practical work of the course logical verification
we use the proof-assistant Coq which is based on typed
lambda calculus.
The theoretic part of logical verification
is concerned with type theory and the
correspondence between logic and typed lambda-calculus
called the "Curry-Howard-De Bruijn isomorphism".
We study various typed lambda calculi and the
corresponding logics.
Course
weeks 36-42 and 44-50: Friday 11.00 - 12.45 in KC 159.
Practical work
weeks 37-42 and 44-50: Wednesday 13.30 - 15.30 in P447 and (part of) P437.
The material for the lectures and the practical work
can be found
here.
Practical work
The practical work is concerned with the proof checker Coq.
Using a web interface we will work on a server at the
Radboud University Nijmegen.
The files containing the exercises will be availble
on this server (and also via the homepage of the course).
The Coq exercises are made during the practical work.
Everyone should hand in his/her solution individually,
but of course it is ok (even recommended) to discuss
your work with others.
The deadline for handing in the exercises is
the next Tuesday (six days after the practical work) at 12.00.
The exercises are graded "pass" or "fail".
In order to participate in the examination
9 out of 12 must be graded "pass".