    Course module   NWIIMC060  Category     Language of instruction   English  Offered by   Radboud University; Faculty of Science; Informatica en Informatiekunde;  Lecturer(s)     Academic year   2021   Period   KW3KW4  (31/01/2022 to 31/08/2022) 
 Starting block   KW3  
 Course mode   fulltime  
 Remarks     Registration using OSIRIS   Yes  Course open to students from other faculties   Yes  Preregistration   No  Waiting list   No  Placement procedure    
     
After successful completion of the course, you will be able to:
 Give mathematical models of imperative and concurrent programming languages using operational semantics.
 Prove properties of imperative and concurrent programs using separation logic.
 Prove properties of type systems for imperative and concurrent programming languages.
 Use the Coq proof assistant to carry out mechanized proofs about program language semantics, separation logic, and type systems.


How can we formally ensure that a program satisfies certain properties? For example, that it does not have memory bugs (such as nullpointer accesses, useafterfree, or buffer overflows) or concurrency bugs (such as data races or deadlocks), that it does not leak confidential information (such as passwords or personal information), or that its output adheres to some mathematical specification?
In this course we study two formalisms to prove such program properties:
 Types. Many programming languages classify program expressions using types, and thereby automatically rule out illbehaved programs like `true + 10`. Modern programming languages like Rust use types to ensure that programs are free of much larger classes or bugs, like memory and concurrency bugs.
 Logic. Using logic one can specify and prove arbitrarily complicated properties of programs. To scale this up to imperative and concurrent programs, we study the formalism of concurrent separation logic (for which the inventors Brookes and O'Hearn received the 2016 GĂ¶del price).
In this course, we use the Coq proof assistant to implement and develop the theory of these formalisms, and apply them to sample programs. In the first three weeks of the course, we will study the basics of Coq, to lay the groundwork for the rest of the course.


 
 Prior knowledge of functional programming (e.g., NWIIBC040 "Functional Programming") and semantics (e.g., NWIIBC026 "Semantics and Correctness" and NWIIBC025 "Semantics and Rewriting") is required.
 Prior knowledge of concurrency is not required.
 Having taken the course NWIIMC010 "Type Theory and Coq" is beneficial, but not required. The present course uses Coq to study imperative programming languages with concurrency, whereas NWIIMC010 studies the foundations of Coq in the context of lambda calculus, type theory, and the formulasastypes correspondence. All Coq exercises in this course are selfcontained and different from those in NWIIMC010.


The final grade is based on the following parts:
 An endproject in the Coq proof assistant
 A written exam.
Both parts have a weight of 50%, and the grade for both parts should be at least a 5.

 


   Instructional modesCourseAttendance Mandatory   Yes 

 TestsExamTest weight   1 
Test type   Exam 
Opportunities   Block KW4, Block KW4 
 ProjectTest weight   1 
Test type   Project 
Opportunities   Block KW4, Block KW4 


  
 
 