(Last Updated:08 April 2015)

**Total Credits: **10

**Level: **Level 4

**Target Students: **MSc and Part III undergraduate students in the School of Computer Science. Also available to Part II undergraduate students in the School of Computer Science subject to Part I performance. Also available to students from other Schools with the agreement of the module convenor. * Available to JYA/Erasmus students.*

**Taught Semesters:**

Semester | Assessment |
---|---|

Spring | Assessed by end of Spring Semester |

**Prerequisites: **Or equivalent knowledge in computer science and mathematics, for example G54FOP or G52MC2 up to 2009/10

Mnem | Title |
---|---|

G51FUN | Functional Programming |

G52IFR | Introduction to Formal Reasoning |

**Corequisites: **None.

**Summary of Content: **

This module is part of the Foundations of Computer Science theme in the School of Computer Science.

This module introduces the student to dependently typed programming as a synthesis of programming and formal reasoning using an existing dependently typed programming language (such as Agda) as a vehicle. Topics covered include the following

- Dependently typed datastructures
- The Curry-Howard Correspondence
- Constructive propositional logic
- Constructive predicate logic
- Metatheory of logical calculi
- Primitive recursion and induction
- Decidability
- Inductively defined relations
- Integrated program correctness
- Certified software tools
- Coinduction

**Method and Frequency of Class: **

Activity | Number Of Weeks | Number of sessions | Duration of a session |
---|---|---|---|

Lecture | 12 weeks | 2 per week | 1 hour |

Practical | 12 weeks | 1 per week | 1 hour |

Activities may take place every teaching week of the Semester or only in specified weeks. It is usually specified above if an activity only takes place in some weeks of a Semester

In addition to the activity details listed there will be a variable practical element amounting to 2-4 hours.

**Method of Assessment: **

Assessment Type | Weight | Requirements |
---|---|---|

Exam 1 | 50 | 2 hour exam |

Coursework 1 | 50 | Four exercises in programming and formal proofs |

**Convenor: **

Dr V Capretta

**Education Aims: **

- To introduce students to the area of dependently typed programming.
- To develop practical skills in developing formal proofs.
- To understand aspects of formal logic relevant for computer aided formal reasoning.
- To be able to judge the role auf formal reasoning.
- To develop transferable skills such as logical thinking and mathematical modelling of problems in Computer Science.

**Learning Outcomes: ****Knowledge and Understanding:**
To learn the rules of formal reasoning.
To understand the role of certified software.
To understand the possibilities and limitations of dependently typed programming
**Intellectual Skills:**
To learn to use a proof assistant to verify software.
To be able to develop formal specifications.
**Professional Skills:**
To be able to develop certified software.
To be able to evaluate tools for dependently typed programming.
To gain experience with engineering of proofs.
To be able to apply dependently typed programming in a software engineering context.
**Transferable Skills:**
To develop reasoning skills.
To learn how to utilize mathematical methods.

**Offering School: **Computer Science

Use the **Back** facility of your browser to return to the previous page.

Return to The University of Nottingham Welcome Page