Theory of programming languages

There are no prerequisites.

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

• B.C. Pierce: “Types and Programming Languages”. The MIT Press 2002.
• J.C. Reynolds: “Theories of Programming Languages”. Cambridge University Press 1998.
• R.M. Amadio & P.-L. Currien: “Domains and λ-calculi”. Cambridge Tracts in Theoretical Computer Science 46. Cambridge University Press, 1998.

The objective of the course is to present
modern, mathematical approach to theory of
programming languages. Students will attain
the ability to analyze programming languages
and the basic concepts related to them.

Knowledge and understanding:
Students learn how to design and analyze
programming languages with formal
mathematical methods.

lectures, tutorials, homeworks

homework, midterm exams, projects, written exam, oral exam

grading: 5 (fail), 6-10 (pass) (according to the Statute of UL)

LUKŠIČ, Primož, HORVAT, Boris, BAUER, Andrej, PISANSKI, Tomaž. Practical E-Learning for the Faculty of Mathematics and Physics at the University of Ljubljana. Interdisciplinary journal of knowledge & learning objects, ISSN 1552-2210, 2007, vol. 3, str. 73-83. [COBISS-SI-ID 14269529]
BAUER, Andrej, STONE, Christopher A. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. V: Computation and logic in the real world : Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 18-23, 2007 : proceedings, (Lecture notes in computer science, ISSN 0302-9743, 4497). Berlin