10.00–10.50 Monday (lecture)
11.10–12.00 Monday (tutorial)
10.00–10.50 Thursday (lecture)
11.10–12.00 Thursday (tutorial)
All lectures and tutorials in FH 1.B31.
Note: Lecture begin in Monday of Week 2.
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
mult_comm
plus_swap
but before proving mult_comm
,
prove Theorem mult_S_r : forall m n, m * S n = m + (m * n).
)
beq_nat_refl
binary_commute
(stretch)
binary_inverse
(stretch)
Lists.v
):
list_funs
list_exercises
update_eq
(stretch)
update_neq
(stretch)
Poly.v
):
poly_exercises
: app_length
more_poly_exercises
fold_length
Tactics.v
):
beq_nat_true
beq_nat_sym
beq_nat_trans
(stretch)
forall_exists_challenge
(stretch)
Logic.v
):
not_both_true_and_false
iff_properties
or_distributes_over_and
dist_not_exists
or dist_exists_or
beq_nat_false_iff
not_exists_dist
(stretch)
classical_axioms
(stretch)
IndProp.v
):
le_exercises
, first five theorems:
le_trans
O_le_n
n_le_m__Sn_le_Sm
Sn_le_Sm__n_le_m
le_plus_l
palindromes
(stretch)
palindrome_converse
(stretch)
pigeonhole_principle
(stretch)
Maps.v
).
ImpExercise.v
:
fact_three_in_coq_is_six
removed and replaced by
ceval_example2
.]
ceval_example2
repeat
bevalR
no_whiles_terminating
stack_compiler
(stretch)
stack_compiler_correct
(stretch)
Equiv.v
):
swap_if_branches
assign_aequiv
CIf_congruence
fold_constants_com_sound
(stretch)
(c ;; WHILE ~b DO c END)
and (REPEAT c UNTIL b END)
equivalent.]
WHILE b DO c END
and IFB b THEN c ;; WHILE b DO c END ELSE SKIP FI
equivalent. Name your theorem while_unroll
. (stretch)
Hoare.v
):
swap_exercise
hoare_repeat
{{P}}c{{Q}} Q /\ ~b ->> P
-------------------------------------
{{P}}REPEAT b UNTIL c END{{Q /\ b}}
Hoare2.v
,
Hoare2-revised.v
)
factorial
factorial_dec
(stretch)
wp
(stretch)
is_wp_formal
(stretch)
Smallstep.v
):
eval__multistep
step__eval
(stretch)
multistep__eval
(stretch)
StlcProp.v
):
types_unique
(stretch)
progress_preservation_statement
MoreStlc.v
):
STLC_extensions
T ::= ... | Empty
t ::= ... | case t of {}
t becomes t'
--------------------------------
case t of {} becomes case t' of {}
Gamma |- t : Empty
-------------------------
Gamma |- case t of {} : T
Typechecking.v
):
STLC_extensions
(stretch).
Please remember the University requirement as regards all assessed work for credit. Details about this can be found on here.
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).
Induction.v
):
Basics.v
to Basics.vo
induction
, proof by cases destruct
plus_assoc
, plus_comm
Lists.v
):
natlist
, app
, app_assoc
Induction.v
):
double_plus
beq_nat_refl
Lists.v
):
list_funs
: nonzeros
list_exercises
: app_nil
Logic.v
):
intro
, elim apply
split
, elim destruct H as [HA HB]
left
, right
, elim destruct H as [HA|HB]
intro
, elim apply
exists
, elim destruct H as [x H']
unfold
and then as for implication
destruct H as []
or exfalso
Maps.v
):
Rel.v
):
Imp.v
):
aexp
, bexp
, aeval
, beval
aevalR
, aeval_iff_aevalR
, (ex) bevalR
aeval
, beval
com
ceval_fun_no_while
ceval
Maps.v
).
ImpExercise.v
:
fact_three_in_coq_is_six
removed and replaced by
ceval_example2
.]
ceval_example2
repeat
bevalR
no_whiles_terminating
stack_compiler
(stretch)
stack_compiler_correct
(stretch)
Maps.v
).
ImpExercise.v
:
fact_three_in_coq_is_six
removed and replaced by
ceval_example2
.]
ceval_example2
repeat
bevalR
no_whiles_terminating
stack_compiler
(stretch)
stack_compiler_correct
(stretch)
Equiv.v
):
swap_if_branches
assign_aequiv
CIf_congruence
fold_constants_com_sound
(stretch)
(c ;; WHILE ~b DO c END)
and (REPEAT c UNTIL b END)
equivalent.]
WHILE b DO c END
and
IFB b THEN c ;; WHILE b DO c END ELSE SKIP FI
equivalent. Name your theorem while_unroll
. (stretch)
Hoare2-revised.v
)
<<->>
.
Smallstep.v
):
tm
, eval
, step
relation
, deterministic
value
strong_progress
, normal_form
,
nf_same_as_value
Module Temp4
multi
, normalising
eval_multistep
Smallstep.v
):
eval__multistep
step__eval
(stretch)
multistep__eval
(stretch)
Stlc.v
):
value
step
subst
has_type
MoreStlc.v
):
Maps.v
)
Types.v
)
Stlc.v
)
MoreStlc.v
):
STLC_extensions
StlcProp.v
):
canonical_forms_bool
,
canonical_forms_fun
progress
appears_free_in
,
free_in_context
context_invariance
substitution_preserves_typing
preservation
E ::= [] t | v [] | if [] then t1 else t2
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.
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 |