University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Undergraduate Course: Functional Programming and Specification (Level 9) (INFR09033)

Course Outline
School School of Informatics College College of Science and Engineering
Course type Standard Availability Available to all students
Credit level (Normal year taken) SCQF Level 9 (Year 3 Undergraduate) Credits 10
Home subject area Informatics Other subject area None
Course website Taught in Gaelic? No
Course description The course has two aims. The first is to provide an introduction to programming in Standard ML including the use of the facilities it offers for structuring programs into modules. Part of this is a review of material from the Functional Programming component of Inf1A, using Standard ML rather than Haskell, but more advanced material is also included. The second aim is to provide an introduction to formal methods for specification and development of programs, using the Extended ML specification framework as a vehicle. Simple proofs of properties of functions are interwoven with the first part of the course to link it with the second part.
Entry Requirements
Pre-requisites Students MUST have passed: Informatics 2A - Processing Formal and Natural Languages (INFR08008) AND Informatics 2B - Algorithms, Data Structures, Learning (INFR08009)
Prohibited Combinations Other requirements Successful completion of Year 2 of an Informatics Single or Combined Degree, or equivalent by permission of the School. Students must have a good background in some programming language together with a familiarity with basic notation from logic (logical connectives, quantifiers, etc.) and proofs using equational reasoning and induction.

MSc students should take the level 10 version of the course (INFR10043).
Additional Costs None
Information for Visiting Students
Pre-requisites None
Displayed in Visiting Students Prospectus? Yes
Course Delivery Information
Not being delivered
Summary of Intended Learning Outcomes
1 - Students will be able to design a representation of an informally-described data structure in ML as a datatype, and translate an informal description of an algorithm into an ML function, making appropriate use of higher-order functions and other characteristic features of the functional programming paradigm.
2 - Students will be able to make effective use of the module facilities in ML to organize programs of about 1000 lines into appropriate units.
3 - Students will be able to use the notation of EML to formulate properties of first-order total ML functions, and to prove such properties using induction and methods of equational reasoning.
Assessment Information
Written Examination 75
Assessed Assignments 25
Oral Presentations 0

Assessed Coursework
Three written assignments, weighted equally: one on ML programming; one on the ML module system; one on specification and proof.

If delivered in semester 1, this course will have an option for semester 1 only visiting undergraduate students, providing assessment prior to the end of the calendar year.
Special Arrangements
Additional Information
Academic description Not entered
Syllabus Functional programming in Standard ML: The functional paradigm. Polymorphic types, static typing and type inference. Recursion and induction. List processing. Higher-order functions. Eager and lazy evaluation. Imperative features. Signatures, structures, functors. Module hierarchy, sharing and data abstraction.

Specification and formal program development in Extended ML: Specification of ML functions and modules. Proving that a program is correct with respect to a specification of its intended behaviour. Refinement of specifications. Formal development of ML programs from EML specifications by modular decomposition and stepwise refinement.

Relevant QAA Computing Curriculum Sections: Comparative Programming Languages, Programming Fundamentals, Software Engineering
Transferable skills Not entered
Reading list * ***L. Paulson. ML for the Working Programmer, second edition. Cambridge University Press, 1996.
* **R. Harper. Programming in Standard ML. Carnegie Mellon University. Soon to be a book. Available on-line.
* ***D. Sannella. Formal program development in Extended ML for the working programmer.
* **S. Gilmore. Programming in Standard ML'97: A tutorial introduction. Edinburgh report ECS-LFCS-97-364, 1997
* *J. Ullman. Elements of ML Programming, second edition. Prentice Hall, 1997.
Study Abroad Not entered
Study Pattern Lectures 20
Tutorials 8
Timetabled Laboratories 0
Non-timetabled assessed assignments 25
Private Study/Other 47
Total 100
Keywords Not entered
Course organiser Dr Marcelo Cintra
Tel: (0131 6)50 5118
Course secretary Miss Tamise Totterdell
Tel: 0131 650 9970
Help & Information
Search DPTs and Courses
Degree Programmes
Browse DPTs
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Important Information
copyright 2011 The University of Edinburgh - 3 April 2011 11:20 am