Course Learning Outcomes
- Understand the common issues in the definition of formal languages, particularly, delineate the issues of syntax, semantics and pragmatics.
- Understand the typed lambda calculus syntax (Church style) and intended semantics
- Learn the idealized functional programming language PCF, which is based on the typed lambda calculus. (At this stage PCF is introduced based on a formal specification of its syntax and an informal description of its semantics.)
- Apply typing rules to infer the type of a given PCF expression.
- Compose programs involving higher-order functions (i.e. functions with function arguments and/or function results) and recursion.
- Understand the axiomatic (equational) approach to semantics of functional languages using the axiomatic semantics of PCF as an example.
- Understand the operational (reductional) approach to semantics of functional languages using the structured operational semantics of PCF as an example.
- Understand the denotational approach to semantics of functional languages using the denotational semantics of PCF as an example.
- Explore the expressive power of PCF and related languages using Turing-computability as the criterion.
- Understand the limitations of PCF and related languages as a sequential programming language.
- Model data types as heterogeneous algebras.
- Specify common abstract data types, such as stacks, queues, lists and trees, by using parametric (generic) types.
- Apply existential types to the specification of abstract data types, introduced to ease many programming tasks.
- Apply extensions to a programming language by syntactic means (e.g. by preprocessing).
- Apply extensions to a programming language, using PCF as an example, by semantic means (e.g. by introducing a new operator not expressible in terms of the core language constructs, such as the fixpoint operator).
- Characterize and compare the functional and imperative programming paradigms.
- Understand the operational approach to semantics of imperative languages using the structured operational semantics of the while language as an example.
- Analyze rigorously the type safety properties of a programming language.
- Understand the role of process calculus in specifying reactive systems.