lemversion

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.

AuthorsDominic 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
LicensesBSD-3-Clause and LGPL-2.1-or-later
Published
Homepagehttp://www.cl.cam.ac.uk/~pes20/lem/
Issue Trackerhttps://github.com/rems-project/lem/issues
MaintainerLem Devs <cl-lem-dev@lists.cam.ac.uk>
Dependencies
Source [http] https://github.com/rems-project/lem/archive/2022-12-10.tar.gz
md5=d5e167df4aaefc3b64ef2dc28436130d
sha512=09b4fc9bdcd3ad95432bb8fbadef9025d3dece6a8d66c390eafc33d6c02ede5044d60291c2b46558905a5941df54a6f8cccf8be7865cbf028f4d9de3042f120e
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/lem/lem.2022-12-10/opam
Required by