Velkommen til Københavns Universitets kursuskatalog
NDAA08006U Semantics and Types
Full Degree Master
C (Mon 13-17 + Wednes 8-17)
Continuing and further
Study Board of Mathematics and Computer
Department of Computer Science
Andrzej Filinski (7-657268767e696e44686d326f7932686f)
Saved on the
MSc Programme in Computer
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 provide a
comprehensive formal basis for developing reliable programs and
programming languages, but also equip 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 specialization.
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.
At course completion, the successful student will have:
General principles for specifying and reasoning about deductive
A selection of specific deductive systems, including
operational semantics, type systems, and program logics.
Techniques for proving properties of individual programs or
program fragments, including equivalences of programs, and their
correctness with respect to a specification.
Techniques for proving properties of whole deductive systems,
including equivalence of semantics, and soundness of program logics
and type systems.
Machine-verifiable representations of deductive-system theory
Reading and writing specifications of deductive systems
relating to programming language theory.
Deciding and proving formal properties of programs or program
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
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
Communicate effectively about programming-language theory, both
for accessing relevant research literature, and convincingly
presenting the results of own work.
Course notes; selected book chapters and articles.
Teaching and learning methods
Lectures, mandatory homeworks, exercise
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
Some exposure to basic formal logic (propositional and first-order
logic, natural deduction) is recommended, but not