NDAA08006U Semantics and Types

Volume 2013/2014
Education
MSc Programme in Computer Science
Content
The aim of the course is to introduce students to the fundamental concepts and tools of modern programming-language theory. This includes the relevant descriptive approaches (formal semantics and type systems), their instantiations and applications to concrete situations, and the mathematical principles for reasoning about them.

The topics covered in the course constitutete a comprehensive formal basis for reliable program and programming-language development, but also provide students with a standardized terminology and conceptual framework for communicating effectively with other developers and researchers, including in follow-up coursework and projects within the PLS competence profile.

The students will be introduced to the following:
  • Basic principles of deductive systems: judgments and inference rules, structural induction, induction on derivations.
  • Operational semantics (big-step and small-step) of simple imperative and functional languages; equivalence of programs; equivalence of semantics.
  • Axiomatic semantics (Hoare logic) of imperative languages; soundness and completeness of program logics.
  • Type systems for functional languages (simple types and selected extensions); type soundness through preservation and progress; type inference.
  • Machine-supported reasoning: proof assistants, proof-carrying code
Learning Outcome
At course completion , the successful student will have:

Knowledge of:
  • General principles for specifying and reasoning about deductive systems.
  • A selection of specific deductive systems, including operational semantics, type systems, and program logics.
  • Techniques for proving properties of, and relating, individual programs or program fragments, including equivalences of programs, and their correctness with respect to a specification.
  • Techniques for proving properties of, and relating, whole deductive systems, including equivalence of semantics, and soundness of program logics and type systems.
  • Machine-verifiable representations of deductive-system theory and metatheory.
Skills in:
  • Reading and writing specifications of deductive systems relating to programming language theory.
  • Deciding and proving formal properties of programs or program fragments.
  • Deciding and proving properties of programming languages or particular language features.
  • Presenting the relevant constructions and proofs in writing, using precise terminology and an appropriate level of technical detail.
Competences to:
  • Reason reliably about correctness or other properties of both imperative and functional programs.
  • Analyze and design (typically domain-specific) programming languages or programming language features in accordance with best practices
  • Communicate effectively about programming-language theory, both for accessing advanced topics from the research literature, and convincingly presenting the results of own work.
Literature
Course notes; selected book chapters and articles
Basic knowledge of discrete mathematics (elementary set theory, proofs by induction), compilers (context-free grammars, syntax-directed compilation) and functional programming (familiarity with ML, Haskell, or Scheme) will be expected.

Some exposure to basic formal logic (propositional and first-order logic, natural deduction) is recommended, but not required.
Lectures, mandatory homeworks, exercise sessions.
  • Category
  • Hours
  • Exam
  • 17
  • Lectures
  • 35
  • Preparation
  • 140
  • Theory exercises
  • 14
  • Total
  • 206
Credit
7,5 ECTS
Type of assessment
Written assignment, 32 hours
Individual, written take-home exam. Submission in Absalon.
Exam registration requirements
5 out of 6 homework sets must be satisfactorily completed in order to participate in the final exam.
Aid
Written aids allowed
Marking scale
7-point grading scale
Censorship form
No external censorship
Several internal examiners
Re-exam
Written assignment + 30 minutes oral examination without preparation. Internal grading on the 7-point scale.
Criteria for exam assesment
See the learning outcome.