sibylfs-lem

Author The Lem Team
Homepage https://bitbucket.org/Peter_Sewell/lem
Maintainer tom.j.ridge@googlemail.com
Dependencies
& ocamlbuild
ocamlfind
Optional dependencies
coq
Published Oct 1, 2015
Source [http] http://bitbucket.org/dsheets/lem/get/0.4.0.tar.gz
9306b3bdc99638d5895156c840033b86
Statistics Installed 6 times in last month.
Edit https://github.com/ocaml/opam-repository/tree/master/packages/sibylfs-lem/sibylfs-lem.0.4.0/opam

SibylFS fork of Lightweight Executable Mathematics for large-scale semantics

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.

Lem is under active development and has been used in several applications, some of which can be found in the examples directory. It is made available under the BSD 3-clause license, with the exception of a few files derived from OCaml, which are under the GNU Library GPL.

Necessary for
sibylfs