Towards a Coq Formalisation of Build Systems
The gene pool of software build systems and various incremental computation frameworks is becoming richer every day. These complex build systems and frameworks use subtle algorithms and are mission-critical, yet to the best of our knowledge they come with no formal proofs of correctness.
A recent ICFP paper “Build Systems à la Carte” presented a definition of correctness for build systems, and modelled several major build systems in Haskell, without exhibiting any proof of their correctness. We build on this work by translating the Haskell abstractions to Coq and making the necessary adjustments to capture the notion of build task acyclicity, which is essential for proving termination.
This is an experience report on on-going work which is very far from being complete. We present our motivation and key abstractions developed so far, and seek feedback and collaboration from the Coq community.
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
16:00 - 17:40
|Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs|
Qinxiang CaoShanghai Jiao Tong UniversityFile Attached
|Teaching Discrete Mathematics to Early Undergraduates with Software Foundations|
|Ltac2: Tactical Warfare|
|Towards a Coq Formalisation of Build Systems|