Capita Selecta of Programming Languages

6 ECTS credits
180 h study time

Offer 1 with catalog number 4019837ENR for all students in the 2nd semester at a (E) Master - advanced level.

Semester

2nd semester

Enrollment based on exam contract

Impossible

Grading method

Grading (scale from 0 to 20)

Can retake in second session

Yes

Taught in

English

Faculty

Faculty of Sciences and Bioengineering Sciences

Department

Computer Science

Educational team

Quentin Pierre Stiévenart
Dominique Devriese (course titular)

Activities and contact hours

26 contact hours Lecture
12 contact hours Seminar, Exercises or Practicals
52 contact hours Independent or External Form of Study

Course Content

– Dependently typed programming en computer-verified proving in Agda
+ Inductive data types with parameters and indices
+ Dependent pattern matching
+ The Identity type
+ Negation
+ Proofs by induction
– Verified and secure compilation: a selection of compiler passes are studied, for example:
+ Register allocation
+ Call lowering
+ Stack spilling
+ Closure conversion
These compiler passes are formalised and studied abstractly and/or in Agda, studying verified and secure compilation properties and proofs.

Course material

Digital course material (Required) : All transparencies and all the code will be provided to the students, Canvas

Additional info

None

Learning Outcomes

General competencies

- The student can explain how a dependently typed programming language can be used for implementing verified algorithms.
- The student is able to formalise and prove simple concepts and results in the Agda dependently-typed programming language.
- The student understands the concepts of verified and secure compilation and formal properties that express them and can apply them to and illustrate them with examples.
- The student can explain, implement and manually execute model versions of the compiler passes studied in this course.
- The student can explain the correctness and security properties and arguments for the compiler passes studied in this course.
- The student is able to make modifications and corrections to correctness arguments and security proofs for model compiler passes, either verbally or implemented in Agda.

Grading

The final grade is composed based on the following categories:
Other Exam determines 100% of the final mark.

Within the Other Exam category, the following assignments need to be completed:

Other exam with a relative weight of 1 which comprises 100% of the final mark.

Additional info regarding evaluation

The evaluation consists for 100% of a course project in which the students formalise and prove concepts and proofs in Agda, related to verified and/or secure compilation.
The students defend the project orally with the teacher during the exam period.
During this defence, their understanding of the concepts taught in this course and their programming and proving skills in Agda will be tested, based on their solution of the course project.

Allowed unsatisfactory mark

The supplementary Teaching and Examination Regulations of your faculty stipulate whether an allowed unsatisfactory mark for this programme unit is permitted.

Academic context