10.00–10.50 Monday (lecture)
11.10–12.00 Monday (tutorial)
10.00–10.50 Thursday (lecture)
11.10–12.00 Thursday (tutorial)
10.00–10.50 Friday (lecture)
11.10–12.00 Friday (tutorial)
All lectures and tutorials in AT 5.08.
Note: Lectures begin Monday of Week 1.
Coursework is worth 25% of your mark. There are five coursework assignments, each worth 5%.
For each assignment you will be given a list of exercises to
complete in the textbook. Copy the relevant files and fill in your
answers. Include a comment at the beginning, listing your
name and which exercises you completed. Mark every
completed exercise by writing (* !!! *)
just before
it. E-mail your files to the instructor. Send all relevant
files: .v, .vo, and .glob. Please ensure your files execute correctly
under Coq!
Some exercises are labeled 'stretch'. These are optional exercises for students who wish an additional challenge.
Note: The coursework is not a light load! But everyone who does the work gets perfect on the exam. (Literally. 100%. That's what proof is for.)
Basics.v
):
factorial
blt_nat
, defined in terms of previously given functions.
blt_nat'
, this time defined directly using recursion.
andb_eq_orb
binary
(stretch)
Induction.v
):
double_plus
Theorem plus_swap : forall m n p, n + (m + p) = m + (n + p).
(Hint: this requires only plus_assoc
and plus_comm
.)
Theorem mult_S_r : forall m n, m * S n = m + (m * n).
Theorem mult_comm : forall m n, m * n = n * m.
Theorem beq_nat_refl : forall n, beq_nat n n = true.
binary
, prove
Theorem binary_comm : forall b, bin_to_nat (incr b) = S (bin_to_nat b).
(stretch)
Lists.v
):
list_funs
list_exercises
update_eq
(stretch)
update_neq
(stretch)
Please remember the University requirement as regards all assessed work. Details about this can be found at:
Furthermore, you are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself, or your group in the case of group practicals).
Induction.v
):
Basics.v
to Basics.vo
induction
, proof by cases destruct
plus_n_O
plus_n_Sm
plus_comm
plus_assoc
Lists.v
):
natlist
, app
, app_assoc
Induction.v
):
double_plus
Theorem plus_swap : forall m n p, n + (m + p) = m + (n + p).
(Hint: this requires only plus_assoc
and plus_comm
.)
Theorem mult_S_r : forall m n, m * S n = m + (m * n).
Theorem mult_comm : forall m n, m * n = n * m.
Lists.v
):
list_funs
: nonzeros
list_exercises
: app_nil
The final examination is worth 75% of your mark.
Because you will be working with Coq throughout the course, you should also have access to Coq for the exam. Unlike most courses with a written exam, TSPL has an online exam where you use the Coq proof assistant to assist and confirm your exam work. If anyone has any questions or concerns, please contact the instructor.
The final exam for TSPL is in December 2017
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh |