Each week of COMP782 has two to three hours of face-to-face class. Classes will be a mixture of lecture-style presentation, discussion and practical demonstration.
REQUIRED AND RECOMMENDED TEXTS AND/OR MATERIALS
COMP782 will follow the book "Software Foundations" by Benjamin Pierce et al. The book consists of annotated programs, proofs and exercises. It can be read in HTML form or the full distribution can be downloaded for formatting as PDF. This book is updated from time to time.
We will use Version 4.0 (May 2016) of the book. Note that more recent versions of the book have been significantly reorganised, split into multiple books, so a current version will not work for this unit.
Students should read the relevant sections of the book and attempt the basic exercises on their own. Class time will be devoted to the main ideas of each chapter and working through a number of exercises. Some basic and more advanced exercises will be set as homework exercises.
UNIT WEBPAGE AND TECHNOLOGY USED AND REQUIRED
COMP782 uses iLearn for delivery of class materials, discussion boards, online selftests, submission of assessment tasks and access to marks and comments. Students should check the iLearn site regularly for unit updates.
Questions regarding the content of this unit should be posted to the appropriate discussion board on iLearn. In particular, any questions which are of interest to all students in this unit should be posted to one of these discussion boards, so that everyone can benefit from the answers.
Coq Proof Assistant
The practical work in this unit involves functional programming and proof construction using the Coq proof assistant (http://coq.inria.fr). Ideally, students should install Coq on a laptop and bring it to class so they can follow along with in-class exercises.
We will use Coq version 8.7.1.
Coq is usually used via a simple IDE platform of which the easiest one is the CoqIDE that is available as part of the Coq distribution. Students who are familiar with Emacs may want to look at the Proof General interface which is similar to CoqIDE but embedded in Emacs.