TypeSynth · Synthetic Methods in Program Verification

Synthetic Methods in Program Verification

Software systems mediate a growing proportion of human activity, e.g. communication, transport, medicine, industrial and agricultural production, etc. As a result, it is urgent to understand and better control both the correctness and security properties of these increasingly complex software systems. The diversity of verification requirements speaks to a need for models of program execution that smoothly interpolate between many different levels of abstraction. Models of program execution vary in expressiveness along the spectrum of possible programming languages and specification logics. At one extreme, dependent type theory is a language for mathematically-inspired functional programming that is sufficiently expressive to serve as its own specification logic. Dependent type theory has struggled, however, to incorporate several computational effects that are common in every-day programming languages, such as state and concurrency. One of the most extreme forms of computational effect is "higher-order mutable state", which is when programs can read and write data as well as entire subroutines to the computer's memory during execution. Programming languages that support these features require very sophisticated specification logics due to the myriad details that must be surfaced in their semantic models. Recently there have been several significant technical advances in mathematical semantics for programming languages that have been ripe for exploitation. For instance, in my doctoral thesis I developed a new technique called Synthetic Tait Computability or “STC” that smoothly combines multiple levels of abstraction into a single language. Inspired by sophisticated mathematical techniques invented in topos theory and category theory for entirely different purposes, STC enables low-level details (even down to execution steps) to be manipulated in a simpler and more abstract way than ever before, making them easier to control mathematically. Perhaps more importantly, the STC method makes it possible to import ideas and techniques from other mathematical fields that are comparatively more developed than programming languages. Another related advance is the use of Synthetic Guarded Domain Theory or "SGDT" as a mathematical language in which to describe and reason about the behavior of computer programs, potentially exhibiting complex interactions with their environment and with other programs. A third advance setting the stage for this project is the development of Univalent Foundations and Homotopy Type Theory, a new and backwards-compatible foundation of mathematics that places symmetries and reversible transformations of mathematical structures in the forefront. The goal of the TypeSynth project has been to combine these three ideas to break a long-standing logjam in the mathematical understanding of computer programming: the denotational semantics and equational separation logic of higher-order mutable state.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз