**High-Level Separation Logic for Low-Level Code**

Jonas Jensen, Nick Benton and Andrew Kennedy.
In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). January 2013.

Separation logic is a powerful tool for reasoning about structured, imperative programs that manipulate pointers. However, its application to unstructured, lower-level languages such as assembly language or machine code remains challenging. In this paper we describe a separation logic tailored for this purpose that we have applied to x86 machine-code programs.

The logic is built from an assertion logic on machine states over which we construct a specification logic that encapsulates uses of frames and step indexing. The traditional notion of Hoare triple is not applicable directly to unstructured machine code, where code and data are mixed together and programs do not in general run to completion, so instead we adopt a continuation-passing style of specification with preconditions alone. Nevertheless, the range of primitives provided by the specification logic, which include a higher-order frame connective, a novel read-only frame connective, and a "later" modality, support the definition of derived forms to support structured-programming-style reasoning for common cases, in which standard rules for Hoare triples are derived as lemmas. Furthermore, our encoding of scoped assembly-language labels lets us give definitions and proof rules for powerful assemblylanguage "macros" such as while loops, conditionals and procedures.

We have applied the framework to a model of sequential x86 machine code built entirely within the Coq proof assistant, including tactic support based on computational reflection.

**Using Coq to Generate and Reason About x86 Systems Code**

Nick Benton, Jonas Jensen and Andrew Kennedy.
Workshop on Syntax and Semantics of Low-Level Languages (LOLA 2012). June 2012.

**Strongly Typed Term Representations in Coq**

Nick Benton, Chung-Kil Hur, Andrew Kennedy and Conor McBride.
To appear in Journal of Automated Reasoning: Special issue on Binding, Substitution and Naming.

There are two approaches to formalizing the syntax of typed object
languages in a proof assistant or programming language. The
*extrinsic* approach is to first define a type that encodes
untyped object expressions and then make a separate definition of
typing judgements over the untyped terms. The *intrinsic*
approach is to make a single definition that captures well-typed
object expressions, so ill-typed expressions cannot even be
expressed. Intrinsic encodings are attractive and naturally enforce
the requirement that metalanguage operations on object expressions,
such as substitution, respect object types. The price is that the
metalanguage types of intrinsic encodings and operations involve
non-trivial dependency, adding significant complexity.
This paper describes intrinsic-style formalizations of both
simply-typed and polymorphic languages, and basic syntactic operations
thereon, in the Coq proof assistant. The Coq types encoding
object-level variables (de Bruijn indices) and terms are indexed by
both type and typing environment. One key construction is the
boot-strapping of definitions and lemmas about the action of
substitutions in terms of similar ones for a simpler notion of
renamings. In the simply-typed case, this yields definitions that are
free of any use of type equality coercions. In the polymorphic case,
some substitution operations do still require type coercions, which we
at least partially tame by uniform use of heterogenous equality.

Coq source for simply-typed language Coq source for polymorphically-typed language

**Some Domain Theory and Denotational Semantics in Coq**

Nick Benton, Andrew Kennedy and Carsten Varming.
22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), August 2009.

We present a Coq formalization of constructive omega-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 CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case.

Talk on typed representation of syntax used in this work, presented at Semantics Lunch at University of Cambridge Computer Laboratory.