Semantics and Types (SaT)
Course 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 provide a comprehensive formal
basis for developing reliable programs and programming languages,
but also equip students with a standardised terminology and
conceptual framework for communicating effectively with other
developers and researchers, including in follow-up coursework and
projects within the PLS study track of the Computer Science
programme.
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 of imperative languages (Hoare logic); soundness and completeness of program logics.
- Denotational semantics, including simple domain theory.
- 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.
MSc Programme in Computer Science
At course completion, the successful student will have:
Knowledge of
- General principles for specifying and reasoning about formal systems.
- A selection of specific formal systems, including semantics, type systems, and program logics.
- Techniques for proving properties of individual programs or program fragments, including equivalence of programs, and their correctness with respect to a specification.
- Techniques for proving properties of whole formal systems, including equivalence of semantics, and soundness of program logics and type systems.
- Machine-verifiable representations of formal-system theory and metatheory.
Skills to
- Read and write specifications of formal systems relating to programming language theory.
- Decide and prove properties of programs or program fragments.
- Decide and prove properties of programming languages or particular language features.
- Present 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.
- Analyse and design (typically domain-specific) programming languages or programming-language features in accordance with best practices
- Communicate effectively about programming-language theory, including accessing relevant research literature, and convincingly presenting the results of own work.
Lectures, theoretical assignments, exercise sessions.
See Absalon for a list of course literature. Expected to be primarily lecture notes, supplemented by selected research articles and other materials.
Comfortable working knowledge of foundational discrete
mathematics and rigorous reasoning (elementary set theory, proofs
by induction), compiler principles (context-free grammars,
syntax-directed compilation), and functional programming
(familiarity with ML/F#, Haskell, or Scheme) will be expected.
General academic qualifications equivalent to a CS or Mathematics
BSc degree are recommended.
Some prior exposure to basic formal logic (propositional and
first-order logic, natural deduction) and logic programming
(Prolog) may be useful, but is not required.
Students will receive detailed written feedback on their homework assignments, as well as a summary of their performance on the exam questions.
As
an exchange, guest and credit student - click here!
Continuing Education - click here!
PhD’s can register for MSc-course by following the same procedure as credit-students, see link above.
- ECTS
- 7,5 ECTS
- Type of assessment
-
Written assignment, 32 hours
- Type of assessment details
- The exam is strictly individual
- Exam registration requirements
-
5 out of 6 weekly assignments must be approved in order to qualify for the exam.
- Aid
- All aids allowed
- Marking scale
- 7-point grading scale
- Censorship form
- No external censorship
Several internal examiners
- Re-exam
-
The re-exam consists of two parts:
1. A 32-hours individual written assignment
2. A 30 minutes oral examination without preparation
The two exams are not weighted, and an overall assessment is provided.
If student did not qualify for the regular exam, qualification for the re-exam can be achieved by submission and approval of equivalent assignments, no later than three weeks before the re-exam date.
Criteria for exam assessment
See Learning Outcome.
Single subject courses (day)
- Category
- Hours
- Lectures
- 35
- Preparation
- 140
- Theory exercises
- 14
- Exam
- 17
- English
- 206
Kursusinformation
- Language
- English
- Course number
- NDAA08006U
- ECTS
- 7,5 ECTS
- Programme level
- Full Degree Master
- Duration
-
1 block
- Placement
- Block 3
- Schedulegroup
-
C
- Capacity
- No limitation – unless you register in the late-registration period (BSc and MSc) or as a credit or single subject student.
- Studyboard
- Study Board of Mathematics and Computer Science
Contracting department
- Department of Computer Science
Contracting faculty
- Faculty of Science
Course Coordinator
- Andrzej Filinski (7-738076848c777c52767b407d8740767d)
Er du BA- eller KA-studerende?
Kursusinformation for indskrevne studerende