Skip navigation
The Australian National University

Principles of Programming Languages COMP6361

Course overview

Course description

The course is built around an investigation of what programming languages are, and the notion of programs as artefacts. Two key aspects of the study of programming languages are their semantics, and their syntax.

We will survey some of the fundamental principles of the semantics and computational behaviour of programs, including the lambda calculus, types and fixed-points. Rigorous proofs of properties of programs, such as are needed for safety-critical software, or for program transformations such as are carried out by optimising compilers, require a formal description of the 'meaning' and behaviour of programs. We will study two of the dominant approaches: denotational semantics and opertional semantics. In each case, standard proof techniques will be developed and applied.

The syntax of programming languages is routinely defined by well-understood means, in terms of formal grammars and their relation to certain classes of automata. We will investigate the algorithms underlying standard automata-bsed compiler generators and make practical use of them to construct simle translators.

Course content

  • The notion of a programming language; programs as artefacts.
  • The lambda calculus: as a model of computation; types and type assignment; recursion; various reduction orders and their consequences.
  • Fixpoint theory: partial orders, monotonicity, lifting; Kleene's recursion theorem; simple recursive domain construction.
  • Denotational and operational semantics of programming languages: basic concepts, structures and techniques of denotational semantics; basic concepts, structures and techniques of opertional semantics; typical proof techniques including structural induction and fixpoint induction.
  • Syntax of programming languages: standard methods for defining the syntax of progamming languages; Chomsky hierarchy of languages and grammars; regular languages and finite state automata; context-free languages and push-down automata; parsing algorithms based on automata; standard tools for generating lexers and parsers.
  • Abstract interpretation: simple examples designed to illustrate some of the the main concepts of the course.

Responsible Officer:  JavaScript must be enabled to display this email address. / Page Contact:  JavaScript must be enabled to display this email address.