Formalizing "Weakest preconditions in fibrations"
Master Project

Project Description

The computation of weakest preconditions is important in the deductive verification of software using Hoare logic. The paper “Weakest preconditions in fibrations” gives a category-theoretic account of weakest preconditions, in terms of fibrations.

The goal of this project is to formalize the results of this paper in the UniMath library, a library of mathematics (and, in particular, category theory) based on univalent mathematics written in the computer proof assistant Coq.

Links:

• Short version of the paper: https://www.sciencedirect.com/science/article/pii/S1571066120300487
• Extended version: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/abs/weakest-preconditions-in-fibrations/657A41FD194D8CC5E4662B71F2E1454E (seems to be behind a paywall)

Project Goals

In this project, you will work on the following goals:

• Learn the basics of univalent mathematics
• Learn to use the computer proof assistants Coq and the library UniMath written in Coq
• Understand the paper “Weakest preconditions in fibrations”
• Formalize the definitions, statements, and proofs of this paper in UniMath

Contacts for the Project

• Benedikt Ahrens (TU Delft)
• Kobe Wullaert (TU Delft)