Lem is a lightweight tool for writing, managing, and publishing large scale semantic definitions. It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems (such as Coq, HOL4, and Isabelle).
Lem resembles a pure subset of Objective Caml, supporting typical functional programming constructs, including top-level parametric polymorphism, datatypes, records, higher-order functions, and pattern matching. It also supports common logical mechanisms including list and set comprehensions, universal and existential quantifiers, and inductively defined relations. From this, Lem generates OCaml, HOL4 and Isabelle code; the OCaml backend uses a finite set library (and does not yet support inductive relations). A Coq backend is in development.
The following example is taken from a model of the POWER multiprocessor architecture that was developed using Lem.
let write_reaching_coherence_point_action m s w =
let writes_past_coherence_point' =
s.writes_past_coherence_point union {w} in
let coherence' = s.coherence union
{ (w,wother) | forall (wother IN (writes_not_past_coherence s)) |
(not (wother = w)) && (wother.w_addr = w.w_addr) } in
<| s with coherence = coherence';
writes_past_coherence_point = writes_past_coherence_point' |>
let sem_of_instruction i ist =
match i with
| Padd set rD rA rB -> op3regs Add set rD rA rB ist
| Pandi rD rA simm -> op2regi And SetCR0 rD rA (intToV simm) ist
end
Lem is already in use at Cambridge and INRIA for research on Relaxed-memory concurrency. We are currently preparing a feature-complete release with back-ends for HOL4, Isabelle/HOL, Coq, OCaml, and LaTeX.
This is a preliminary release of Lem which is not yet feature complete. It is currently released under a restrictive license, but we intend to use an open source or free software license for later, more complete releases.
Abstract. Many ITP developments exist in the context of a single prover, and are dominated by proof effort. In contrast, when applying rigorous semantic techniques to realistic computer systems, engineering the definitions becomes a major activity in its own right. Proof is then only one task among many: testing, simulation, communication, community review, etc. Moreover, the effort invested in establishing such definitions should be re-usable and, where possible, irrespective of the local proof-assistant culture. For example, in recent work on processor and programming language concurrency (x86, Power, ARM, C++0x, CompCertTSO), we have used Coq, HOL4, Isabelle/HOL, and Ott---often using multiple provers simultaneously, to exploit existing definitions or local expertise.
In this paper we describe Lem, a prototype system specifically designed to support pragmatic engineering of such definitions. It has a carefully designed source language, of a familiar higher-order logic with datatype definitions, inductively defined relations, and so on. This is typechecked and translated to a variety of programming languages and proof assistants, preserving the original source structure (layout, comments, etc.) so that the result is readable and usable. We have already found this invaluable in our work on Power, ARM and C++0x concurrency.
Lem shares many of the goals of our Ott tool: both emphasize source readability, and multi-prover compatibility. However, Lem is a general-purpose specification language, whereas Ott is a domain-specific language for writing specifications of programming languages (i.e., inductive relations over syntax). Thus, Ott supports rich user-defined syntaxes, whereas Lem supports functional programming idioms.
Lem and Ott are complementary; we eventually hope to merge the two projects by having Ott generate Lem specifications, instead of Coq, HOL4, and Isabelle itself.