[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

RFP: Isabelle -- generic proof assistant

 hoping you can pack this into Debian,
i've sent the wnpp ;)

-------- Forwarded Message --------
Subject: RFP: Isabelle -- generic proof assistant
Date: Thu, 2 Nov 2017 11:02:25 +0800
From: GengYu Rao <zouyoo@outlook.com>
To: submit@bugs.debian.org
CC: lcp@cl.cam.ac.uk, nipkow@in.tum.de

Package: wnpp
Severity: wishlist

* Package name    : Isabelle
   Version         : 2017
   Upstream Author :  University of Cambridge
* URL             : http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html
* License         : BSD-3-Clause
  Description     :

Isabelle/HOL allows to turn executable specifications directly into code in
SML, OCaml, Haskell, and Scala.
Isabelle comes with a large theory library of formally verified 
including elementary number theory , analysis , algebraand set theory .
Also provided are numerous examples arising from research into formal 
Isabelle/jEdit is the default user interface and Prover IDE for Isabelle.
you can use it as an IDE for sml:)

btw,This package included many add-on components under contrib/*
as you can see, this package is being actively developed.

I hope someone may pack this into debian.


GengYu Rao

Reply to: