Course Objectives
- Understand the connection between typed lambda calculus and functional programming.
- Understand the connection between syntax, semantics and pragmatics of a programming language.
- Understand the operational, denotational and axiomatic approaches to the definition of (both functional and imperative) programming language semantics with emphasis on operational semantics.
- Understand the role of type theory in giving semantics to programming languages and reasoning about its essential properties.
- Analyze the given programs (in both functional and imperative styles), written in an hypothetical programming language, using the operational specification of the language.
- Apply formal semantics to verify the (partial) correctness of a program with respect to a given input-output specification.
- Evaluate the expressive power and limitations of a programming language.
- Devise recursive data types and use them in recursive programming.
- Devise new abstract data types and use available ones to facilitate a given programming task.
- Apply extensions to a programming language by syntactic and semantic means.