6 ECTS credits
180 u studietijd
Aanbieding 1 met studiegidsnummer 4019837ENR voor alle studenten in het 1e en 2e semester met een verdiepend master niveau.
– 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.
None
- 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.
De beoordeling bestaat uit volgende opdrachtcategorieën:
Examen Andere bepaalt 100% van het eindcijfer
Binnen de categorie Examen Andere dient men volgende opdrachten af te werken:
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.
Deze aanbieding maakt deel uit van de volgende studieplannen:
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Artificiële Intelligentie
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Multimedia
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Software Languages and Software Engineering
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Data Management en Analytics
Master in Applied Sciences and Engineering: Computer Science: Artificial Intelligence (enkel aangeboden in het Engels)
Master in Applied Sciences and Engineering: Computer Science: Multimedia (enkel aangeboden in het Engels)
Master in Applied Sciences and Engineering: Computer Science: Software Languages and Software Engineering (enkel aangeboden in het Engels)
Master in Applied Sciences and Engineering: Computer Science: Data Management and Analytics (enkel aangeboden in het Engels)