Catalogue of Modules, University of Nottingham

G54DTP Dependently Typed Programming
(Last Updated:08 April 2013)

Year  10/11

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:

SemesterAssessment
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

MnemTitle
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

Module Web Links:
   
  • module web page

    • Method and Frequency of Class:

    ActivityNumber Of WeeksNumber of sessionsDuration of a session
    Lecture 12 weeks2 per week1 hour
    Practical 12 weeks1 per week1 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

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

    Method of Assessment: 

    Assessment TypeWeightRequirements
    Exam 1 50 2 hour exam 
    Coursework 1 50 Four exercises in programming and formal proofs 

    Convenor: 
    Dr V Capretta

    Education Aims:  

    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.

    Module Catalogue Search for another module

    [UoN Welcome Page] Return to The University of Nottingham Welcome Page