N. Benton, L. Birkedal, A. Kennedy, and C. Varming. Formalizing domains, ultrametric spaces and semantics of programming languages.
We describe a Coq formalization of constructive ω-complete partial orders (ω-cpos) and bisected complete ultrametric spaces, up to and including the inverse-limit construction of solutions to mixed-variance recursive equations in categories enriched over ω-cppos and categories enriched over bisected complete ultrametric spaces. We show how these mathematical structures may be used in formalizing semantics for three representative programming languages. Specifically, we give operational and denotational semantics for both a simply-typed call-by-value language with recursion and an untyped call-by-value language, establishing soundness and adequacy results in each case. We then define a Kripke logical relation over a recursively-defined metric space of worlds to give an interpretation of types over a step-counting operational semantics for a language with recursive types and general references.
Many different mathematical structures are used in programming language semantics, some of which are built on others (e.g. cpos being a further specialization of partial orders) and many of which support similar constructions like cartesian products, exponentials, etc. The formalization applies two techniques to manage this complexity. The first is a design pattern, due to Garillot et al. [2009], for mixin-style packaging of mathematical structures. The second is the formalization of a certain amount of category theory, enabling us to work with abstract and reusable definitions, lemmas and notations. This combination enables us to use generic syntax for common constructions (e.g. cartesian products), and generic proofs of properties of these constructions.
Nick Benton, Andrew Kennedy, and Carsten Varming. Some Domain Theory and Denotational Semantics in Coq. In TPHOLs, pages 115–130, 2009.
We present a Coq formalization of constructive ω-cpos (extending earlier work by Paulin-Mohring) up to and including the inverse limit construction of solutions to mixed-variance recursive domain equations, and the existence of invariant relations on those solutions. We then define operational and denotational semantics for both a simply typed call-by-value language with recursion and an untyped call-by-value language, and establish soundness and adequacy results in each case.
L. Birkedal, R.L. Petersen, R.E. Møgelberg, and C. Varming. Operational Semantics and Models of Linear Abadi-Plotkin Logic.
We present a model of Linear Abadi and Plotkin Logic for parametricity based on the operational semantics of LILY, a polymorphic linear lambda calculus endowed with an operational semantics. We use it to formally prove definability of general recursive types in LILY and to derive reasoning principles for the recursive types.
Carsten Varming and Lars Birkedal. Higher-order separation logic in Isabelle/HOLCF. In Proceedings of MFPS XXIV, 2008.
We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct assertions, e.g., primitive recursion, least or greatest fixed points etc. The higher-order logic enables us to show non-trivial algorithms correct without having to extend the semantics of the language as was done previously in verifications based on first-order separation logic (SBR and Yang). We provide non-trivial examples to support this claim and to show how the higher-order logic enables natural assertions in specifications. To support abstract reasoning we have implemented rules for representation hiding and data abstraction as seen in BBT. The logic is represented as lemmas for reasoning about the denotational semantics of the programming language. This follows the definitional approach common in HOL theorem provers, i.e., the soundness of our model only relies on the soundness of Isabelle/HOL. We use our formalization to give a formally verified proof of Cheney’s copying garbage collector using a tagged representation of objects. The proof generalizes the results in [SBR]. The proof uses an encoding of the separation logic formula this(h) to capture the heap from before the garbage collection and thus shows another novel use of higher-order separation logic.
- [BBT] Biering, B., L. Birkedal and N. Torp-Smith. BI-Hyperdoctrines, Higher-order Separation Logic, and Abstraction.
- [SBR] N. Torp-Smith, L. Birkedal, and J. Reynolds. Local reasoning about a copying garbage collector. ACM Transactions on Programming Languages and Systems, 2006.
- [Yang] Hongseok Yang. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm.
Teaching assistant at Carnegie Mellon University
TAed 15-122 Principles of Imperative Computation for Frank Pfenning. The course gave the students an introduction to imperative programming. We first introduced C0, a type safe subset of C, then concepts from Hoare logic, and finally C. From Hoare logic we taught pre-, post-conditions, and loop invariants. This enabled the students to show partial correctness of their programs. Furthermore, the C0 frame work enabled the students to execute assertions about shapes, greatly improving their bug finding capabilities. Finally we introduced C and some of the higher-order features of C needed in good engineering.
Internship at Microsoft Research Cambridge
Developed trace models for concurrent programming languages in Coq.
Internship at Microsoft Research Cambridge
Developed constructive domain theory in Coq.
Teaching assistant at Carnegie Mellon University
TAed 15-312 Principles of Programming Languages for Bob Harper. The course introduced basic concepts of modern functional programming languages to the students. Much emphasis was given to type safety.
Research programmer at ITU
Grading Assistant at University of Copenhagen
PhD Thesis
In my PhD thesis I am developing a logic that enable programmers to naturally express protocols, i.e., the expected interaction between concurrent processes, and then show that their programs adhere to such protocols.
In current logics such as Concurrent Separation Logic
and Rely-Guarantee logics, finding invariants
describing the shared state can be difficult and when
a programmer finds a suitable invariant, the
specifications of the given processes are often global, and
thus tied to the specific context a given process is
executed in. A simple example is the specification:
{x = 0} with r do x := x+1 || with r do x := x+2 {x = 3}
The specification needed to show safety of the left
process must include an auxiliary variable to keep
track of the right process. In this classic example
substitution can provide the answer, but in general
that it not the case. It should also be noted that
substitution rules are absent in a great number of
logics designed to show safety of of such programs.
In my thesis proposal I illustrate how to specify the interaction between a process and its environment without explicitly mentioning the environment. This enables a programmer to use the same specification of heap safety of a process in many different contexts. I then propose the use of graph like structures to reason about protocol safety, i.e., safety of the interaction specifications of the processes in the program. The key new idea is that it is possible to reason separately about heap safety and protocol safety, and that this leads to proofs that can easily be reused in many different environments.
Personal
I am a graduate student in the POP group in the Computer Science Department at Carnegie Mellon University.
I can often be found in my office: GHC 6505
CMU CSD
5000 Forbes Avenue
Pittsburgh PA 15213
USA
You can call me at: +1 (412) 805-2055 or from Denmark +45 4694 9344. When I am in Europe you can reach me at: +45 5260 6605.
You can also email me: varm...@gmail.com (my last name at gmail.com).
