lemversion Documentation on ocaml.org
Lem is a tool for lightweight executable mathematics
Lem is a tool for lightweight executable mathematics, for writing, managing, and publishing large-scale portable semantic definitions, with export to LaTeX, executable code (currently OCaml) and interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL).
It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems.
| Authors | Dominic Mulligan, Francesco Zappa Nardelli, Gabriel Kerneis, Kathy Gray, Peter Boehm, Peter Sewell, Scott Owens, Thomas Tuerk, Brian Campbell, Shaked Flur, Thomas Bauereiss, Stephen Kell, Thomas Williams, Lars Hupel and Basile Clement |
|---|---|
| Licenses | BSD-3-Clause and LGPL-2.1-or-later |
| Published | |
| Homepage | http://www.cl.cam.ac.uk/~pes20/lem/ |
| Issue Tracker | https://github.com/rems-project/lem/issues |
| Maintainer | Lem Devs <cl-lem-dev@lists.cam.ac.uk> |
| Dependencies |
|
| Conflicts | |
| Source [http] | https://github.com/rems-project/lem/archive/refs/tags/2026-05-01.tar.gz sha256=87782e0887613d5ec3d52831762f4537cd46f4817b03ec37e80831f52a5b7f03 sha512=5372418b2451ad44a91e8324926661b19fb402b7a33981977bc680be9d33f9c2ccaa2d2bf146c573fcfc5eb4d660cf06c6ac8278313ec52c560ee86b3fc5cfc6 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/lem/lem.2026-05-01/opam |
