Queen's School of Computing

CISC 465/3.0 Foundations of Programming Languages

Original Author: Bob Tennent
Last Revised: September 25, 2006

Calendar Description

Syntax and semantics. Classification of programming languages. The language of while programs. The typed lambda calculus. Recursive definitions and domain theory.

Prerequisites: CISC 204/3.0, 223/3.0, 260/3.0.

Objectives

Designers, implementers, and serious users of a programming language need a complete and accurate understanding of the semantics (the intended meaning) as well as the syntax (the form) of every construct of that language. There is a well-developed and widely-known mathematical theory of formal languages which supports accurate description of (the context-free aspects of) the syntax of programming languages, and correct implementation of scanners and parsers. But the descriptions of context-dependent aspects of syntax (such as scope and type checking) and of semantics in reference manuals and language standards are almost always inadequate because they are based primarily on implementation techniques and intuition.

Rigorous mathematical theories of the semantics and context-dependent aspects of the syntax of programming languages are needed to support correct description and implementation of languages, systematic development and verification of programs, analysis of existing programming languages, and design of new languages that are simpler and more regular. This course is an introduction to these theories.

Topics

Introduction

  • context-free and context-dependent syntax
  • denotational, operational and logical approaches to semantics

Simple Imperative Languages

  • denotational semantics of
    • elementary control structures
    • variables and assignment
    • while loops
  • operational semantics of a simple imperative language
  • program specifications and program proofs
  • validity of program-correctness axioms and rules

Simple Functional Languages

  • denotational semantics of
    • function application and definition
    • recursion
  • domain theory
  • operational semantics of a simple functional language
  • quantification and substitution
  • validity of program equivalences and derivation rules

Procedural Languages

  • combining the syntax and semantics of imperative and functional languages

Possible Textbooks

  • R. D. Tennent. Semantics of Programming Languages. Prentice-Hall International, 1991.

  • J. C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998.

  • G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, Cambridge, Mass., and London, England, 1993.

  • H. R. Nielson and F. Nielson. Semantics with Applications, a Formal Introduction. John Wiley, Chichester, England, 1992.

  • D. A. Schmidt. Denotational Semantics, A Methodology for Language Development. Allyn and Bacon, Newton, Massachusetts, 1986.