Course Schedule

DTP
The tentative schedule of the upcoming lectures can be found below. This may still change!

%TABLE{cellpadding="5" dataalign="left"}%
| *Date* | *Topic* | *Resources* | *Slides*|
| 23 Apr | Introduction | | [[%ATTACHURL%/slides1.pdf][slides]] |
| 25 Apr | Lecture cancelled | | |
| 30 Apr | No Lecture - Queen's Day | | | 
| 02 May | Coq intro | [[%ATTACHURL%/demo.v][Coq demo file]] | [[%ATTACHURL%/slides2.pdf][slides]] |
| 07 May | Software foundations - Basics|  | |
| 09 May | No Lecture - Ascension Day | | | 
| 14 May | Software foundations - Lists, Polymorphism | | | 
| 16 May | Software foundations - Polymorphism, Generalizing IH | | [[%ATTACHURL%/slides3.pdf][slides]] | 
| 21 May | Verification challenge - coaching session: Jaap van der Plas, Wout Elsinghorst & Pepijn Kokke, Koen Rutten | | |
| 23 May | Verification challenge - coaching session: Tom Tervoort & Stijn van Drongelen, Marco Eilers & Robert Schmidtke | | |
|             | Joao Pizani Flor & Liewe van Binsbergen, Matthijs Steen & Tibor Bremer | | |
| 28 May | Software foundations - Propositions | | | 
| 30 May | Software foundations - Logic | | | 
| 04 Jun | Software foundations - Fancy recursion | | | 
| 06 Jun | Agda | | | 
| 11 Jun | Presentations: Robert Schmidtke | | | 
|            | Matthijs Steen | | |
|            | Marco Eilers | | |
| 13 Jun |  Presentations: Tom Tervoort | | | 
|            | Joao Paulo Pizani Flor | | |
|            | Stijn van Drongelen | | |
| 18 Jun |  Presentations: Wout Elsinghorst | | | 
|            | Jaap van der Plas | | | 
|            | Liewe Thomas van Binsbergen | | |
| 20 Jun |  Presentations: Tibor Bremer | | | 
|            | Koen Rutten | | |
|            | Pepijn Kokke | | |
| 08 Jul | Verification project presentations | | |
<!--
| 24 Apr| Introduction: dependent types and the Curry-Howard isomorphism| [[http://www.jstor.org/stable/37448][Constructive mathematics and computer programming]]| [[http://www.cs.uu.nl/wiki/bin/viewfile/DTP/CourseSchedule?rev=1;filename=DTP_lecture_1.pdf][DTP_lecture_1.pdf]] |
| | |  [[http://www.andres-loeh.de/LambdaPi][A tutorial implementation of a dependently typed lambda calculus]]| |
| 26 Apr| Implementing a simple dependently typed language| | [[http://www.cs.uu.nl/wiki/bin/viewfile/DTP/CourseSchedule?rev=1;filename=DTP_lecture_2.pdf][DTP_lecture_2.pdf]] |
|            |  |  | [[http://www.cs.uu.nl/wiki/bin/viewfile/DTP/CourseSchedule?rev=1;filename=demo.v][Coq demo]] |
| 01 May| Software foundations| [[http://www.cis.upenn.edu/~bcpierce/sf/][Software foundations homepage]] | Completed the first chapter, Basics|
|             | | | [[%ATTACHURL%/DTP_lecture_3.pdf][DTP_lecture_3.pdf]] |
| 03 May | Lecture cancelled | | |
| 08 May | Software Foundations - Lists, data structures in Coq | | |
| 10 May | Software Foundations - Polymorphism  | | |
| 15 May | Software Foundations - Generalizing induction hypotheses | | |
| 17 May | Software Foundations - Coq best practices and Propositions | | [[%ATTACHURL%/DTP_lecture_4.pdf][DTP_lecture_4.pdf]] |
| 05 Jun | Agda demo (continued) | | [[%ATTACHURL%/demo.agda][demo.agda]] |
| 07 Jun | Programing finger trees in Coq -- Nikos Savvidis | | |
|            | Idris -- Hidde Verstoep| | |
| 12 Jun | Epigram: Practical programming with dependent types -- Tim Soethout | | |
|            | Algebra of Programming using Dependent Types -- Joao Alpuim | | |
| 14 Jun | Mixing Induction and Coinduction -- Gabe Dijkstra | | |
|            | Total Parser Combinators -- Augusto Passalaqua | | |
| 19 Jun | MiniAgda: Integrating Sized and Dependent Types -- Jurriën Stutterhem | | |
|            | LTL types as FRP -- Nikolaos Bezirgiannis  | | |
| 21 Jun | A Formal Comparison of Approaches to Datatype-Generic Programming -- Frank Wijmans | | |
|            | Type-safe diff for families of datatypes -- Andreas | | |
| 26 Jun | The Power Of Pi -- Beerend Lauwers | | |
|            | Ornamental Algebras, Algebraic Ornaments -- Tim Kuipers  | | |
| 28 Jun | No lecture scheduled | | | 
!-->

<!--
| 15 Sep | Introduction to Agda |
| 22 Sep | Agda tutorials |
| 29 Sep | Agda tutorials |
| 06 Oct | Bas (Martin-Lof type theory, Curry-Howard isomorphism); induction principles; discussion Assignment 1 |
| 13 Oct | Ruud (Tutorial Implementation), Steven (Generic Programming) |
| 20 Oct | Alessandro (Coinduction, Total Parser Combinators), Paul (Lemmachine); discussion Assignment 2 |
| 27 Oct | Observational Equality, Ring Solver; discussion Assignment 3 |
| 03 Nov | Bram (Scrapping your Inefficient Engine) |
| 10 Nov | student presentations |


| 09 Sep | Inductive families, examples | read [[#UlfTutorial][UlfTutorial]] 1-2, [[Assignments][Assignment 0]] |
| 11 Sep | propositional equality, Fin| read [[#UlfTutorial][UlfTutorial]] rest, try to prove that Vec and Vec' are isomorphic |
| 16 Sep | Curry-Howard, introduce library | work on  [[Assignments][Assignment 1]]|
| 18 Sep | discuss [[#UlfTutorial][UlfTutorial]] | [[Assignments][Assignment 1]], install standard library, look at !Relation.Binary.EqReasoning |
| 23 Sep | no meeting | |
| 25 Sep | no meeting | |
| 30 Sep | discuss [[#UlfTutorial][UlfTutorial]], Erik/Paul (equational reasoning) | [[Assignments][Assignment 2]] |
| 02 Oct | Chris/Sebastiaan (type system), Mathijs/Tom (eliminators) | read Power of Pi |
| 07 Oct | Jeroen/Joeri (decidable equality), Kasper (various things) | |
| 09 Oct | discuss Power of Pi | |
| 14 Oct | Sebastiaan (positivity), discuss Data.Star | look at Data.Star ([[http://sneezy.cs.nott.ac.uk/fun/nov-07/R-star.pdf][Conor's talk]]) |
| 16 Oct | Erik (MAlonzo), discuss Data.Star| [[Assignments][Assignment 3]] |
| 21 Oct | codata | |
| 23 Oct | Coq | install Coq, [[Assignments][Assignment 4]] |
| 28 Oct | Ynot | read Ynot paper |
| 30 Oct | final discussion and conclusion | |
| 04 Nov | exam in BBL-426 | |
-->

-- Main.WouterSwierstra - 23 Apr 2013