Lattice Theory for Parallel Programming

Description: Lattice theory is one of the most useful mathematical theories to describe and prove properties of computer programs. Lattice theory occurs with great success in the history of computer science starting with denotational semantics (what is a program from the mathematical perspective), abstract interpretation (how to verify a program is correct) and more recently in parallel and distributed computing with conflict-free replicated data types (CRDTs) and constraint solving on GPU (how to program with clients and threads having an incomplete view of the global state). CRDTs are widely used to program highly-available services for cloud storage, mobile clients and applications for collaborative editing of a document.

This course is given in the Master in High Performance Computing at the University of Luxembourg with Pr. Bruno Teheux (department of mathematics) and Yi-Nung Tsao (teaching assistant).

The course is self-contained, only basic knowledge of set theory and logic is necessary. Half of the course consists in lattice theory (given by Bruno) and the other half on applications of lattice theory (given by myself).

  • Lectures on lattice theory (by Bruno) are available here
  • Lecture 1: Overview of the Course [pdf]
  • Lecture 2: Conflict-free Replicated Data Type [pdf] with a laboratory [pdf]
  • Lecture 3: More Conflict-free Replicated Data Type [pdf] with a laboratory [pdf]
  • Lecture 4: Parallel Lattice Programming [pdf]
  • Lecture 5: Abstract Satisfaction [pdf]
  • Lecture 6: Neural Network Verification [pdf]
  • Lecture 7: Abstract Interpretation [pdf]
The course is complemented by two graded projects:
  • Design of Parallel Algorithms with Lattice Data Type [pdf]
  • Neural Network Verification with Abstract Interpretation [pdf]