Search
Now showing items 1-3 of 3
Introduction to Categories and Categorical Logic
The aim of these notes is to provide a succinct, accessible introduction to some of the basic ideas of category theory and categorical logic. The notes are based on a lecture course given at Oxford over the past few years. ...
Trace Properties from Separation Logic Specifications
We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Separation logic with abstract predicates ...
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
(2021-05-06)
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to ...