Lem, a tool for lightweight executable mathematics

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).

The language combines features familiar from functional programming languages with logical constructs. From functional programming languages we take pure higher-order functions, general recursion, recursive algebraic datatypes, records, lists, pattern matching, parametric polymorphism, a simple type class mechanism for overloading, and a simple module system. To these we add logical constructs familar in provers: universal and existential quantification, sets (including set comprehensions), relations, finite maps, inductive relation definitions, and lemma statements. Then there are facilities to let the user tune how Lem definitions are mapped into the various targets (by declaring target representations and controlling notation, renaming, inlining, and type classes), to generate witness types and executable functions from inductive relations, and for assertions.

Lem typechecks its input and can generate executable OCaml, theorem prover definitions in Coq, HOL4, and Isabelle, typeset definitions in LaTeX, and simple HTML. It supports a program-like development cycle, with fast type checking of Lem source files.

Papers

Code

Lem is hosted on Bitbucket here. Use git to download the latest source code with the command: git clone https://bitbucket.org/Peter_Sewell/lem.git

Documentation

Examples

The examples directory in the repository contains or points to several major examples of Lem usage:

Development team

Kathy Gray, Gabriel Kerneis Dominic Mulligan, Scott Owens, Peter Sewell, Thomas Tuerk.

Past contributors: Peter Boehm, Thomas Williams, Francesco Zappa Nardelli.

Lem and Ott

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. The two can be used together in some cases: Ott can now generate Lem specifications.

History

Validate HTML 4.01 Strict