sibylfs-lem

SibylFS fork of Lightweight Executable Mathematics for large-scale semantics
Description

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.

Install
Published
02 Oct 2015
Sources
sibylfs-lem-0.4.0.tar.gz
md5=9306b3bdc99638d5895156c840033b86
Dependencies
Reverse Dependencies