Topics for G54FOP Coursework Academic Year 2012--2013
=====================================================

* Basic Program Correctness

  Basic introduction to the notion of program correctness and how
  to use Hoare logic to prove that a program meets its specification. 

  - Chapters 1, fragments of 2, and 3 of John Reynolds: Theories of
    Programming Languages (Available form the library.)
  - Another possibility: Chapters 1-3 of Michael J. C. Gordon:
    Programming Language Theory and its Implementation
  - Wikipedia: 
      + http://en.wikipedia.org/wiki/Program_correctness
      + http://en.wikipedia.org/wiki/Hoare_logic
      + A complementary perspective:
        http://en.wikipedia.org/wiki/Curry-Howard_correspondence

* Basic Data Flow Analysis

  The task here is to give an introduction to data flow analysis
  and how it can be related to a small step operational semantics
  to prove analyses correct.

  Starting points:
  - Sections 1.1 - 1.3, 2.1 - 2.4 of Flemming Nielson, Hanne Riis
    Nielson, Chris Hankin: Principles of Program Analysis

* Abstract Interpretation

  Starting points:
  - Section 1.5, Chapter 4 of Flemming Nielson, Hanne Riis
    Nielson, Chris Hankin: Principles of Program Analysis
  - Wikipedia
  - Papers on applications, such as strictness analysis

* Type and Effect Systems

  - Section 1.6, Chapter 5  of Flemming Nielson, Hanne Riis
    Nielson, Chris Hankin: Principles of Program Analysis

* Abstract Machine Semantics

  We have studied operational semantics in this module. This is
  a fairly "machine-like" approach to explaining the meaning of
  programming language constructs as it describes the step by
  step transformation of terms into a final answer. If the
  semantics is stated in a deterministic way, it is usually quite
  straight forward to turn the semantics into an interpreter
  implemented, say, in a functional language.

  However, because the operational rules often have premises,
  the resulting machines are rather sophisticated in that some
  form of recursive rule invocation is involved. And the
  machinery for controlling this is not readily visible
  (essentially a control stack).

  Is there a more basic approach to semantics? There is:
  it is usually referred to as Abstract Machines.

  The task here is to explain this approach by looking
  at an abstract machine for the lambda calculus (say,
  the SECD machine), explaining how it works, and
  relating to the other styles of operational semantics
  (transition semantics or structured operational semantics,
  natural semantics) and discussing pros and cons (e.g.
  for what purposes are the different styles suitable).

  Starting points:

  - Chapter 1 of Carl A. Gunter: Semantics of Programming Languages
    (Available from the library.)
  - Olivier Danvy. A Rational Deconstruction of Landin's SECD Machine
    BRICS technical report. http://www.brics.dk/RS/03/33/

* Calculation of (functional) programs from specifications

  Starting points:

  - E.g. Caclculating Functional Programs by Jeremy Gibbons
    (advanced, available on-line)