Kursussøgning, efter- og videreuddannelse – Københavns Universitet

Videresend til en ven Resize Print Bookmark and Share

Kursussøgning, efter- og videreuddannelse

Semantics and Types (SaT)

Practical information
Study year 2016/2017
Time
Block 3
Programme level Full Degree Master
ECTS 7,5 ECTS
Course responsible
  • Andrzej Filinski (7-69766c7a826d72486c7136737d366c73)
  • Department of Computer Science
Course number: NDAA08006U

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 standardized terminology and conceptual framework for communicating effectively with other developers and researchers, including in follow-up coursework and projects within the PLS 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 (Hoare logic) of imperative languages; 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.

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 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 and metatheory.

 

Skills to:

  • Read and write specifications of deductive systems relating to programming language theory.
  • Decide and prove formal 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.
  • 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 relevant research literature, and convincingly presenting the results of own work.

 

Recommended prerequisites

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, Scheme or F#) will be expected.

Some exposure to basic formal logic (propositional and first-order logic, natural deduction) is recommended, but not required.

Sign up


As an exchange, guest and credit student - click here!

Continuing Education - click here!

Education

MSc Programme in Computer Science

Studyboard

Study Board of Mathematics and Computer Science

Course type

Single subject courses (day)

Duration

1 block

Schedulegroup

C
---- SKEMA LINK ----

Teaching and learning methods

Lectures, mandatory homeworks, exercise sessions.

Capacity

No limit

Language

English

Literature

Course notes; selected book chapters and articles.

Workload

Category Hours
Lectures 35
Theory exercises 14
Exam 17
Preparation 140
English 206

Exam

Type of assessment

Written assignment, 32 hours
Individual, written take-home exam.

Aid

Written aids allowed

Marking scale

7-point grading scale

Criteria for exam assessment

See the learning outcome.

Censorship form

No external censorship
Several internal examiners

Re-exam

If student is not qualified then qualification can be achieved by hand-in and approval of equivalent homework sets.

Written assignment (32 hours) + 30 minutes oral examination without preparation.

Mere information om kurset
Er du BA- eller KA-studerende?
Er du bachelor- eller kandidat-studerende, så find dette kursus i kursusbasen for studerende:

Kursusinformation for indskrevne studerende