Logical Relations for Program Verification

In an economy as relentlessly digital as the modern worldwide one, in
which everything from toasters to interpersonal communications to
global financial services are computerised, the need for formally
verified software cannot be overestimated. Formal verification uses
mathematical techniques to prove that programs actually perform the
computations they are intended to perform (e.g., that text editors
really do save files when a SAVE command is issued or that automatic
pilots really do correctly execute flight plans) and also avoid
performing unintended ones (e.g., leaking credit card details or
launching nuclear weapons without authorisation). Since programmers
make 15 to 50 errors per 1000 lines of code, and since repairing them
accounts for some 80% of project expenses, the ever-increasing size
and sophistication of programs makes formal verification increasingly
critical to modern software development.

Mathematical reasoning lies at the core of all formal verification,
and so is crucial for building truly secure and reliable software.
One of the key techniques for formally verifying properties of
software systems uses logical relations. Logical relations provide a
means of deriving properties of a software system directly from the
system itself; as a result, they can be used to prove important
properties of programs, programming languages, and language
implementations. Logical relations have been developed for core
fragments of many modern programming languages and verification
systems. They are currently extended to richer programming languages
and properties by constructing plausible variants of the definitions
of logical relations for appropriate core fragments and checking that
the mathematical theory goes through. But as languages and properties
to be proved have become increasingly sophisticated and expressive,
this ad hoc approach has become both difficult and unsustainable. It
has also led to an enormous constellation of complicated and
non-reusable logical relations that "work" for particular language
features, rather than their principled and transferrable development
from fundamental principles. In short, logical relations have
struggled to keep pace with developments in programming languages,
with the obvious consequences for security and reliability of software
systems.

We aim to revolutionise the landscape of logical relations by
providing framework for their development and use that is principled,
conceptually simple, reusable, and uniform (rather than ad hoc). Our
framework will be capable of both describing the wide array of logical
relations already used in existing applications and prescribing new
logical relations for future ones. It will be based on the
mathematical concept of comprehension for a fibration, which has not
previously been identified as a key ingredient in
the construction of logical relations. Our use of it thus
distinguishes our framework from all other treatments of logical
relations in the literature. Comprehension allows explicit representation of logical properties of
languages within those languages themselves. This means that our
framework will be implementable, so we will produce a logic for
deriving consequences of logical relations and a prototype
implementation of that logic in a modern interactive theorem
prover. This will allow users to experiment with our framework, and
allow their experiences with it to feed back into its
foundations. We will also apply our new framework for logical
relations to cutting-edge problems that are the focus of active
research and for which there is presently no consensus on the way
forward. Successful application of our framework will show that it can
solve problems that are the focus of active research, as
well as open up unanticipated new research directions. Conversely, the
practical applications we pursue will raise challenges that prompt us
to further refine its foundations

The long-term impact of this research is to contribute to our ability
to formally verify properties of programs. Logical relations are a
key technique for proving properties of programs, programming
languages, and programming language implementations. Although the
proposed research --- namely, providing a principled, comprehensive,
and predictive foundation for logical relations --- does not lend
itself to immediate industrial uptake, we have devised the following
five-point plan for maximising its impact.

- We will publish in top international venues so as to disseminate
our ideas and results to a wide audience and, at conferences, get
feedback and network.

- This year Dr Johann organised a workshop on logical relations that
attracted most of the leaders in the field. We will organise
another such workshop for early on in the grant period. We expect
this follow-up workshop to attract a similarly strong group of
participants, which will enable us to disseminate our ideas to
precisely those people most likely to be interested in them.

- Collaborate extensively with leaders in the field so as to ensure
our ideas receive attention even while in development. To
facilitate this, we have teamed up with five leaders in various
aspects of the proposed research. Not only will their input help
keep the research outwardly focused, but it will mean that
dissemination into the community takes place even as the research
is being developed.

- Undertake carefully designed work packages that show case the
benefits of our ideas. In particular, each work package not only
contains great science, but also demonstrates something specific
about our approach, such as how the different degrees of freedom it
engenders can be exploited in applications or how it can be used to
solve state-of-the-art problems that have attracted the attention
of researchers around the world.

- Provide a logical system for reasoning with logical relations,
together with an implementation of it, so as to make our ideas
accessible to the wider community. This will be crucial if we are
to have as great an impact as we desire because not all researchers
will have our technical background. Indeed, with our logical system
and implementation, users can access our results without any
knowledge whatsoever of its category-theoretic foundations.

It is worth noting that Reynolds' seminal presentation of logical
relations still forms the basis of current research on logical
relations nearly 30 years after it was first developed. Overall, our
goal is to give a new foundation of logical relations. If we are
successful, we can expect our ideas to remain central to the subject
--- both academically and in terms of commercial exploitation --- for
an equally long time. That certainly would be impact!