Skip to main content

Module

CSC3332 : Programming Language Design and Verification (Inactive)

  • Inactive for Year: 2020/21
  • Module Leader(s): Dr Stephen Riddle
  • Owning School: Computing
  • Teaching Location: Newcastle City Campus
Semesters
Semester 1 Credit Value: 20
ECTS Credits: 10.0

Aims

Programming languages come and go - if you make a career in computing, there is no doubt that you will have to learn languages which do not even exist today. This is in addition to literally thousands of general purpose languages, there are those tailored for specific applications like gaming, virtual reality, text layout, robotics, etc. Sadly, many languages embody one new idea (e.g. objects, concurrency, remote execution) but are significantly *worse* than their predecessors in other respects

The principal aim of this module is to communicate ways of understanding and documenting the key ideas in a language. The material should equip you to make sense of the many languages you will meet in your career. If you design new languages, they will benefit from you being able to manipulate the key concepts.

Furthermore, to make sure the complexities (and scale) of language design are addressed, you will also be trained in practical aspects of formal modelling and verification. For this we will use a well-founded approach following a set of mature formal tools and techniques within software engineering.

Outline Of Syllabus

Introduction - syntax versus semantics
Syntax - (concrete versus abstract; context conditions).
Semantics (meaning)
(Focusses on the "Structured Operational Semantics" technique.)
Revision/other approaches

Covering large definitions (PL/I, Ada, Java) and different (to SOS) approaches

Introduction
- nature of software verification principles (correctness, abstraction, refinement, design decisions, documented assumptions, model-based testing, etc.)
- understanding expertise required and costs involved; identifying the right technique to the task at hand.

Modelling and Specification
- key notions of functional programming: induction, recursion, termination, datatypes, type classes, referentially transparent, etc.
- basics notions of verification tools: Isabelle 101, structural induction, tooling for language design.
- elicitation and proof of properties of interest: compilation x interpretation agreement, language transformations, etc.
- improved language-design decisions: type system extensions (e.g. security-types, etc.), feature extension (e.g. OO + concurrency), etc.
- code-contracts and programming correctness reasoning
Prototyping:
- prototype code generation of correct compiler

Teaching Methods

Module leaders are revising this content in light of the Covid 19 restrictions.
Revised and approved detail information will be available by 17 August.

Assessment Methods

Module leaders are revising this content in light of the Covid 19 restrictions.
Revised and approved detail information will be available by 17 August.

Reading Lists

Timetable