Assignments
| Number |
Date Out |
Date In |
Links |
| Homework 1 |
5 Sep |
12 Sep, before class |
PDF,
SML starter file,
PDF solutions,
SML solutions
|
| Homework 2 |
12 Sep |
19 Sep, before class |
Agda file,
Solutions
|
| Homework 3 |
19 Sep |
26 Sep, before class |
Agda file,
Solutions |
| Homework 4 |
26 Sep |
3 Oct, before class |
Agda file,
Solutions |
| Homework 5 |
3 Oct |
10 Oct, before class |
Agda file,
Solutions |
| Take-home Midterm |
10 Oct |
Friday, 18 Oct, 5pm |
Agda file,
Solutions
|
| Homework 6 |
25 Oct |
Fri 1 Nov, noon |
Agda file,
Solutions |
| Homework 7 |
1 Nov |
Thurs 7 Nov, 10:30am |
Preliminaries.agda,
Agda file,
Solutions
|
| Homework 8 |
7 Nov |
Mon 18 Nov, 4pm |
Agda file,
Solutions
|
| Final Project Proposal |
7 Nov |
Thurs 14 Nov, 10:30am |
|
| Final Project |
14 Nov |
Fri 13 Dec, 5pm |
|
Some final project ideas:
-
Read these
notes about merge-sorting trees. Implement the algorithm in Agda,
and prove some properties of it (that it returns a sorted tree, that it
has the correct elements).
-
Read
these notes
on regular expression matching. There is a very detailed account of a
somewhat intricate proof of correctness for the algorithm. Formalize it
in Agda.
-
Read some of this paper
or these notes
on type systems that keep track of scientific units, and then make a
library for units of measure in Agda.
-
Read
about type
providers
(also
see this
paper for an implementation in another dependently typed
programming language), and implement something like this in Agda.
That is, write Agda code that guesses types given some examples of some
data. You can start simple (e.g., with comma-separated list of values of
various types), and you don't actually need to hack the Agda
compiler---to start, you can assume the data is in an Agda file.
-
For those who have taken DPL: do a simple type safety proof for a
programming language. I can show you how to represent a programming
language in Agda.
