Home
Education Page
Course schedule
Assignments
Papers
VerificationChallenge
Agda
Coq
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
Assignments
DTP
The following assignments should be completed *individually* and submitted by email. They will show up here as the course progresses. %TABLE{cellpadding="5" dataalign="left"}% | *Assignment* | *Deadline* | | [[%ATTACHURL%/BasicExc.v][Basic exercises]] | 15 May | | [[%ATTACHURL%/PolyListExc.v][Polymorphism and list exercises]] | 29 May | | [[%ATTACHURL%/LogicExc.v][Logic and propositions]] | 10 Jun | | [[%ATTACHURL%/exercises.agda][Agda exercises]] | 21 Jun | <!-- | *Assignment* | *Summary* | *Deadline* | | Lambda Pi | Add new data types to the Lambda Pi interpreter | 7 May | | | [[%ATTACHURL%/LambdaPi.pdf][Problem description]] | | | | [[%ATTACHURL%/LP.hs][Source code]] | | | Basics exercises | Exercises nandb, andb3, factorial, blt_nat, (simpl_plus), | | | | plus_id_exercise, mult_1_plus, zero_nbeq_plus_1, andb_true_elim2, basic_induction| | | | double_plus, beq_nat_refl, mult_comm, evenb_n_oddb_Sn, (more_exercises), | | | | plus_swap', binary, decreasing | 16 May | | List exercises | all exercises | 16 May | | Polymorphism | poly_exercises, split, currying, partition, map_rev, flat_map, silly_ex, apply_exercise1, override_neq, sillyex1, sillyex2, app_ass', apply_exercise2, plus_n_n_injective, combine_split, filter_exercise, apply_exercises, forall_exists_challenge | 29 May | | Generalizing induction hypotheses | all exercises | 29 May| | Prop | plus_one_r', ExSet, four_ev, ev_plus4, double_even, ev_sum, inversion_practice, ev_ev_even, ev_ev_plus, ev_MyProp, palindromes, subsequence| 8 Jun | | Logic | and_assoc, even_ev, conj_fact, or_distributes_over_and_2, contrapositive, not_both_true_and_false, not_eq_beq_false,not_exists_dist, dist_exists_or, all_forallb, nostutter| 8 Jun | | Agda | [[%ATTACHURL%/exercises.agda][Agda Exercises]] | 18 Jun | !--> <!-- | [[%ATTACHURL%/Assign0.pdf][Assignment 0]] | first steps in Agda | 09 Sep | | [[%ATTACHURL%/Assign1.pdf][Assignment 1]] | vectors, Fin, matrices | 18 Sep | | [[%ATTACHURL%/Assign2.pdf][Assignment 2]] | heaps, team tasks | 30 Sep | | [[%ATTACHURL%/Assign3.pdf][Assignment 3]] | eliminators, zipper | 16 Oct | | [[%ATTACHURL%/Assign4.pdf][Assignment 4]] | lambda calculus | 23 Oct | | [[%ATTACHURL%/Assign5.pdf][Assignment 5]] | Coq | 30 Oct | -->