| Kursusnavn (dansk): | Programming Language Seminar |
| Kursusnavn (engelsk): | Programming Language Seminar |
| Semester: | Forår 2017 |
| Udbydes under: | cand.it., softwareudvikling og -teknologi (sdt) |
| Omfang i ECTS: | 7,50 |
| Kursussprog: | Engelsk |
| Kursushjemmeside: | https://learnit.itu.dk |
| Min. antal deltagere: | 1 |
| Forventet antal deltagere: | 0 |
| Maks. antal deltagere: | 30 |
| Formelle forudsætninger: | The BSc in Software Development courses Second Year Project:Functional Programming and Discrete Mathematics or equivalent. |
| Læringsmål: | This course has two major parts — a regular course covering select state-of-the art in programming languages and software verification followed by a project.
After the course the students are expected to be able to:
• Characterise some recent developments in programming languages and verification technology,
• account for the practical applications of the covered constructs, and
• With respect to the latter, the student must be able to summarize, evaluate, discuss and contrast the studied techniques, and be able to reflect on their utility and apply them to cases studies.
On the basis of the project, the students are expected to be able to:
• apply relevant methods and techniques in the chosen project,
• argue for the overall design-decisions in, and correctness properties of, the project, and
• relate the project to the underlying theory. |
| Fagligt indhold: | The subject of the course is programming language foundations and technologies, with special attention to advanced technologies that are likely to influence software practice over the next ten years.
The contents of the course is structured in two themes.
1. Axiomatic Reasoning about Models and Programs
In particular, their pragmatic use in program design via model-driven development, implementation, validation, and verification.
The material and structure for this part of the course will come from Benjamin Pierce's Software Foundations course using the Coq proof assistant.
http://www.cis.upenn.edu/~bcpierce/sf/
https://coq.inria.fr/
2. Verifying imperative programs
We will cover operational and axiomatic semantics of imperative programming languages. We will use Hoare Logic and Separation Logic to write specifications for and prove the correctness of imperative programs. |
| Læringsaktiviteter: | 14 ugers undervisning bestående af forelæsninger, øvelser og vejledning The course period is 16 weeks quarter time (7.5 ects). The course consists of:
• Lectures and exercises (approximately 10 weeks), covering the themes of the course.
• A project done in groups of 1-3 students (approximately 6 weeks), within one of the themes, resulting in a project report.
Study structure
This course is part of the SDT specialization Programming Languages. |
| Obligatoriske aktivititer: | During this course students will be required to hand in mandatory assignments, that need to be completed/approved before being eligible to attend the examination.
• There will be eight weekly hand-in assignments, all of which you must pass before you start your projects. An exact date will be given at the start of the course.
• There will be one mandatory presentation of software verification tools used in industry and/or academia. An exact date will be given at the start of the course.
Be aware: The student will receive the grade NA (not approved) at the ordinary exam, if the mandatory activities are not approved and the student will use an exam attempt
• A project spanning approximately six weeks must be handed in. An exact handing date will be given at the start of the course.
Be aware: The student will receive the grade NA (not approved) at the ordinary exam, if the mandatory activities are not approved and the student will use an exam attempt |
| Eksamensform og -beskrivelse: | D22: Aflevering med mundtlig eksamen suppleret af aflevering., (7-scale, external exam) The project report must be presented in an oral exam, where questions may be asked in all themes of the course.
The duration of this oral exam is 30 minutes.
|
| Litteratur udover forskningsartikler: | Software Foundations by Benjamin Pierce (http://www.cis.upenn.edu/~bcpierce/sf/) |
| | |
Kursusoversigt