Programs, Proofs, and Tactics in the Coq Proof Assistant (MSc. def.)

Date: 14:30 07/09-15
Location: Turing-230
Host(s): Christian Clausen

During this Masters thesis defence I will give a brief overview to selected parts of my thesis.

The thesis studies the Coq proof assistant (and programming language) with focus on definability, both in the function language and in the tactic language, the former will be the focus in the defence. Coq puts certain constraints on functions, such as having exactly one decreasing argument, or being total. These constraints can be circumvented by using some elegant tricks which is what I will present.

The plan for the defence is:
14:30-15:00 Presentation by Christian, and questions from audience
15:00-15:30 Questions from censor (Andrzej Filinski) and examiner (Olivier Danvy)

Evaluation

Login to evaluate.