[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Savannah-register-public] [task #7611] Submission of Poussin proof assi
From: |
nicolas marti |
Subject: |
[Savannah-register-public] [task #7611] Submission of Poussin proof assistant |
Date: |
Sat, 05 Jan 2008 02:07:34 +0000 |
User-agent: |
Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.8.1.11) Gecko/20071221 Firefox/2.0.0.11 |
URL:
<http://savannah.nongnu.org/task/?7611>
Summary: Submission of Poussin proof assistant
Project: Savannah Administration
Submitted by: alalme
Submitted on: samedi 05.01.2008 à 11:07
Should Start On: samedi 05.01.2008 à 00:00
Should be Finished on: mardi 15.01.2008 à 00:00
Category: Project Approval
Priority: 5 - Normal
Status: None
Privacy: Public
Percent Complete: 0%
Assigned to: None
Open/Closed: Open
Discussion Lock: Any
Effort: 0.00
_______________________________________________________
Details:
A new project has been registered at Savannah
This project account will remain inactive until a site admin approves or
discards the registration.
= Registration Administration =
While this item will be useful to track the registration process, *approving
or discarding the registration must be done using the specific Group
Administration
<https://savannah.nongnu.org/siteadmin/groupedit.php?group_id=9631> page*,
accessible only to site administrators, effectively *logged as site
administrators* (superuser):
* Group Administration
<https://savannah.nongnu.org/siteadmin/groupedit.php?group_id=9631>
= Registration Details =
* Name: *Poussin proof assistant*
* System Name: *poussin*
* Type: Official GNU software
* License: GNU General Public License v2 or later
----
==== Description: ====
Poussin is a GPL proof assistant based on the Curry-Howard isomorphism. Its
underlying lambda calculus is an extension of a simple version of the Calculus
of Construction (CoC, the base calculus for the first versions of the Coq
proof assistant), with inductive types and recursive functions. Thus, poussin
is closely related to Coq (even in the name, as Coq means roaster). Poussin is
first a educational project which aims at learning the theoretic and
engineering aspects of a proof assistant based on type theory. It is mainly
composed of a kernel (that contains mainly the type checker), and a user
interface to interactively enters terms. The whole project is implemented in
the Ocaml programming language.
==== Tarball URL: ====
http://savannah.gnu.org/submissions_uploads/poussin.tgz
_______________________________________________________
Reply to this item at:
<http://savannah.nongnu.org/task/?7611>
_______________________________________________
Message posté via/par Savannah
http://savannah.nongnu.org/
- [Savannah-register-public] [task #7611] Submission of Poussin proof assistant,
nicolas marti <=