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)