Mechanized Denotational Semantics using Synthetic Category Theory
Abstract
Software bugs in critical systems such as health, transportation or military devices can cause failures that cause severe damage to human beings and property. To mitigate and eliminate these bugs, computer scientists develop programming languages and formal logics where software systems can be mathematically proven to behave correctly and be free of errors. Further, these proofs themselves can be machine-checked to be free from errors in mathematical reasoning. Many languages and logics today are designed using a mathematical theory called category theory which studies how abstract systems can be combined together and how to correctly reason about the behavior of the combined system. Such logics can be proven sound using a technique called denotational semantics which develops models that show that every proof in the logic exhibits a genuinely true theorem. Category theory has provided powerful and reusable proof techniques that have facilitated great advances in development of logics, but relatively few of these proofs are themselves machine-checked. This requires placing a high level of trust in humans that prior results are being correctly used in large-scale software proofs. Further while these techniques are powerful, using them properly requires a great deal of expertise, requiring a high level of mathematical sophistication from the programmers verifying their system. In this proposal we propose to develop a reusable library of machine-checked category theory proofs and apply them to the verification of language implementations. To support this, we will build on prior work on a synthetic approach to category theory, a kind of domain specific language for category theory definitions and proofs that helps manage the natural complexity that arises in formalizing the mathematical arguments commonly found in category theoretic proofs. This will help to support easier development of verified software from reusable components.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 14, 2024
- Source ID
- FA95502310760
Entities
People
- Max New
Organizations
- Air Force Office of Scientific Research
- Board of Regents of the University of Michigan
- United States Air Force