Package: wnpp Severity: wishlist Owner: Bo YU <tsu.yubo@gmail.com> X-Debbugs-Cc: debian-devel@lists.debian.org * Package name : lem Version : 2022-12-10 Upstream Contact: Lem Devs <cl-lem-dev@lists.cam.ac.uk> * URL : https://github.com/rems-project/lem * License : BSD-3 Programming Lang: OCaml Description : Lem semantic definition language 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, though the generated Coq is not necessarily idiomatic). It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems. The language, originally based on a pure fragment of OCaml, combines features familiar from functional programming languages with logical constructs. From functional programming languages we take pure higher-order functions, general recursion, recursive algebraic datatypes, records, lists, pattern matching, parametric polymorphism, a simple type class mechanism for overloading, and a simple module system. To these we add logical constructs familiar in provers: universal and existential quantification, sets (including set comprehensions), relations, finite maps, inductive relation definitions, and lemma statements. Then there are facilities to let the user tune how Lem definitions are mapped into the various targets (by declaring target representations and controlling notation, renaming, inlining, and type classes), to generate witness types and executable functions from inductive relations, and for assertions. ------------------------->>>>------------------- The package is a dependency of sail[0] and linksem[1] and then I will maintian it under Debian ocaml team. [0]: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1065419 [1]: https://github.com/rems-project/linksem -- Regards, -- Bo YU
Attachment:
signature.asc
Description: PGP signature