Undergraduate Course: Types and Semantics for Programming Languages (INFR10040)
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 10 (Year 4 Undergraduate) |
Credits | 10 |
| Home subject area | Informatics |
Other subject area | None |
| Course website |
http://course.inf.ed.ac.uk/tspl |
Taught in Gaelic? | No |
| Course description | Type systems and semantics are mathematical tools for precisely describing aspects of programming language. A type system imposes constraints on legal programs in order to guarantee their safe execution, whilst a semantics specifies what a program will do when executed. This course gives an introduction to the main ideas and methods of type systems and semantics. This enables a deeper understanding of existing programming languages, as well as the ability to design and specify new language features. |
Information for Visiting Students
| Pre-requisites | None |
| Displayed in Visiting Students Prospectus? | No |
Course Delivery Information
|
| Delivery period: 2013/14 Semester 2, Available to all students (SV1)
|
Learn enabled: No |
Quota: None |
Web Timetable |
Web Timetable |
| Course Start Date |
13/01/2014 |
| Breakdown of Learning and Teaching activities (Further Info) |
Total Hours:
100
(
Lecture Hours 20,
Summative Assessment Hours 2,
Programme Level Learning and Teaching Hours 2,
Directed Learning and Independent Learning Hours
76 )
|
| Additional Notes |
|
| Breakdown of Assessment Methods (Further Info) |
Written Exam
75 %,
Coursework
25 %,
Practical Exam
0 %
|
| No Exam Information |
Summary of Intended Learning Outcomes
1 - Read and understand the presentation of operational semantics and type systems via inference rules for lambda calculus, and be able to modify such a presentation to include a new language feature, such as state and exceptions.
2 - State and prove the theorems that relate big-step and small-step semantics, and the preservation and progress theorems that link operational semantics and type systems.
3 - Exploit the connection between logic and type systems, where propositions correspond to types and proofs correspond to programs; understand how conjunction corresponds to products, disjunction to sums, and implication to functions.
4 - Explain the differences between informal and formal semantics of programming languages, and between the operational, denotational and axiomatic approaches to formal semantics.
5 - Read a formal semantics for a small programming language written in operational or denotational style, interpret it in informal terms, and predict how a given program will behave according to the semantic definition.
6 - Write a formal semantics for a programming language in the operational style, given a careful informal description of the language, and explain how any inadequacies in the informal description have been addressed in the formal one. |
Assessment Information
Written Examination 75
Assessed Assignments 25
Oral Presentations 0
Assessment
Short exercises each week.
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
| None |
Additional Information
| Academic description |
Not entered |
| Syllabus |
Type systems for programming languages
* Untyped and simply-typed lambda calculus. Variable binding.
* Small step and big step semantics.
* Progress and preservation theorems.
* Products, sums, and list types.
* Reference types and exceptions.
* Subtyping. Subsumption and its understanding as inclusion or coercion.
Formal semantics for programming languages
* Principles of operational, denotational and axiomatic semantics.
* Key concepts of semantics: compositionality, adequacy, observational equivalence, full abstraction and definability.
* Case study: operational semantics for a fragment of Java.
Relevant QAA Computing Curriculum Sections: Comparative Programming Languages, Compilers and Syntax Directed Tools, Programming Fundamentals, Theoretical Computing |
| Transferable skills |
Not entered |
| Reading list |
* Benjamin Pierce, et al, Software Foundations, 2012. [Available online, required reading: http://www.cis.upenn.edu/~bcpierce/sf/]
* Benjamin C Pierce, Types and Programming Languages, MIT Press, 2002. [recommended reading]
* Benjamin C Pierce, editor, Advanced Topics in Types and Programming Languages, MIT Press, 2005. [recommended reading]
* G. Winskel, The Formal Semantics of Programming Languages: an introduction. MIT Press, 1993. [recommended reading]
|
| Study Abroad |
Not entered |
| Study Pattern |
Not entered |
| Keywords | Not entered |
Contacts
| Course organiser | Dr Mary Cryan
Tel: (0131 6)50 5153
Email: mcryan@inf.ed.ac.uk |
Course secretary | Miss Kate Farrow
Tel: (0131 6)50 2706
Email: Kate.Farrow@ed.ac.uk |
|
© Copyright 2013 The University of Edinburgh - 10 October 2013 4:36 am
|
University Homepage