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.

Published: 12 Dec 2022

Dependencies (6)

  1. num
  2. zarith >= "1.4"
  3. conf-findutils build
  4. ocamlbuild build
  5. ocamlfind build & >= "1.5.1"
  6. ocaml >= "4.07.0"

Reverse Dependencies (3)

  1. libsail
  2. linksem
  3. sail < "0.15"

Conflicts

    None
Lem is a tool for lightweight executable mathematics

Install

Documentation www.cl.cam.ac.uk Edit opam file

Authors

  1. D
    Dominic Mulligan
  2. F
    Francesco Zappa Nardelli
  3. G
    Gabriel Kerneis
  4. K
    Kathy Gray
  5. P
    Peter Boehm
  6. P
    Peter Sewell
  7. S
    Scott Owens
  8. T
    Thomas Tuerk
  9. B
    Brian Campbell
  10. S
    Shaked Flur
  11. T
    Thomas Bauereiss
  12. S
    Stephen Kell
  13. T
    Thomas Williams
  14. L
    Lars Hupel
  15. B
    Basile Clement

Maintainers

  1. L
    Lem Devs <cl-lem-dev@lists.cam.ac.uk>

Sources

2022-12-10.tar.gz
md5=d5e167df4aaefc3b64ef2dc28436130d
sha512=09b4fc9bdcd3ad95432bb8fbadef9025d3dece6a8d66c390eafc33d6c02ede5044d60291c2b46558905a5941df54a6f8cccf8be7865cbf028f4d9de3042f120e