[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: Gecko/20071221 Firefox/


                 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



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
<> page*,
accessible only to site administrators, effectively *logged as site
administrators* (superuser):

* Group Administration

= 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: ====


Reply to this item at:


  Message posté via/par Savannah

reply via email to

[Prev in Thread] Current Thread [Next in Thread]