##
Course Outline |
||

Introduction to the dependently typed functional programming language of Coq as well as its formal language for mathematical definitions and theorems. Introduction to higher-order logic, interactive theorem proving. Development of verified software using the Coq system.

Week |
Date |
Topics |

1 | Sep 07/12 | Introduction, Principle of functional programming and interactive theorem proving |

2 | Sep 14/19 | Functions as proofs, Proofs as functions |

3 | Sep 21/26 | Coq basics |

4 | Sep 28/Oct 03 | Programming in Coq I |

5^{*} |
Oct 05/17 | Programming in Coq II |

6 | Oct 19/24 | Verification of functional programs in Coq I, (Test 1) |

7 | Oct 26/31 | Verification of functional programs in Coq II |

8 | Nov 02/07 | Verification of functional programs in Coq III |

9 | Nov 09/14` | Algebraic theories in Coq I |

10 | Nov 16/21` | Algebraic theories in Coq II |

11 | Nov 23/28 | Algebraic theories in Coq III, (Test 2) |

12 | Nov 30/Dec 05 | Further features of Coq, Review |

COSC 5V90 Home Page