COMP3610: Principles of Programming Languages

(6 credit points) Group C
Second Semester

Course Coordinator

Name: Michael Stevens
Email: michael.stevens@anu.edu.au
Room: CSIT (108) N311

Prerequisites

COMP2600; COMP2100; 6 credit points of 2000-level mathematics, statistics or econometrics.
Incompatible with COMP3065, COMP3039, COMP3040

Course Description

This is an advanced course in programming languages for students who possess substantial knowledge of conventional languages. (Ideally, students will be familiar with C and Haskell, and have non-trivial experience with these, or similar, languages)

The unit will provide an introduction to the underlying theoretical principles of programming languages, and the use of the lambda calculus, fixpoint theory and formal methods of proof in programming languages. It will give the student some experience of Haskell and the use of complier development tools such as flex and bison.

As well as exploring these tools the course will introduce the students to ideas that apply across languages. If a program requires rigorous correctness proofs, such as saftey-critical software, or compilers, it is necessary to have a formal description of the meaning of the language. The unit will discuss formal semantics in general and will focus on a widely used system - denotational or structured operational. The course will also touch on some well-understood meas of defining the syntax of a programming language, with the use of formal grammars, and the relation between these grammars and some classes of automata.

Learning Outcomes

At the completion of this unit the student will be able to:

1.

Manipulate and generate lambda-terms, extending a system such as Church numerals; check and assign types to lambda terms.

2.

Solve simple recursive equations by determining the limit of the Kleene fixpoint construction.

3.

Design and extend operational and denotational definitions for basic programming language constructs

4.

Prove properties of programs by various formal means, including structural and fixpoint induction.

5.

Demonstrate and explain correspondences between grammars, languages and automata.

6.

Given the context free grammar of a language, produce a parser using standard parser and lexer generater tools.

Assessment

Assignments (30%), broken into two assignments worth 10% and 20% Final exam (70%)