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.