The course covers the theory of programming
languages with empahsis on mathematical
methods for specification of programming
languages and analysis of their properties. The
following topics are covered:
-
concrete and abstract syntax, lexical
analysis and parsing as translation of
concrete syntax to abstract syntax -
inductive definitions, definitions given in
terms of judgements and rules of
inference -
proofs by structural induction on
abstract syntax and on the structure of a
derivation -
inductive datatypes as an example of
use of structural definitions and
structural induction -
operational semantics as an inductively
specified relation, small-step and big-
step semantics -
functional programming languages:
recursive definitions, eager and lazy
languages, static analysis, type checking,
safety as a consequence of progress and
termination lemmas, significance of
safety in practice -
polymorphism, parametric
polymorphism and Hindley-Milner type
inference -
imperative programming languages,
specification and proofs of correctness -
denotational semantics: domains and
continuous maps, existence of fixed
points, denotational semantics of a
functional language, interpretation of
recursion as fixed points -
optional topics: object-oriented
programming languages, parallel
computing, logic programming
