taskSavannah Administration - Tasks: task #7611, Submission of Poussin proof...

 
 

task #7611: Submission of Poussin proof assistant

Submitter:  nicolas marti <alalme>
Submitted:  Sat 05 Jan 2008 02:07:33 AM UTC
   
 
Should Start On:  Fri 04 Jan 2008 03:00:00 PM UTC Should be Finished on:  Mon 14 Jan 2008 03:00:00 PM UTC
Category:  Project Approval Priority:  * 5 - Normal
Status:  Done Privacy:  Public
Assigned to:  Beuc Open/Closed:  Closed
* Mandatory Fields

Add a New Comment Rich Markup
   

Sun 06 Jan 2008 08:08:31 AM UTC, comment #2: 

Also note that I approved the project as non-GNU. Please check http://www.gnu.org/help/evaluation.html to submit your project for GNU Evaluation.

Regards.

Sylvain Beucler <Beuc>
Sun 06 Jan 2008 08:07:19 AM UTC, comment #1: 

Hi,

I approved your project.

Before to upload your code at Savannah, please remember to add a copy of the GFDL as a section of your documenation (this is mentioned in your .tex license block, but the section is yet to be added).

Regards.

Sylvain Beucler <Beuc>
Sat 05 Jan 2008 02:07:33 AM UTC, original submission:  

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



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


nicolas marti <alalme>

 

(Note: upload size limit is set to 16384 kB, after insertion of the required escape characters.)

Attach Files:
   
   
Comment:
   

No files currently attached

 

Depends on the following items: None found

Items that depend on this one: None found

 

Carbon-Copy List
  • -email is unavailable- added by Beuc (Posted a comment)
  • -email is unavailable- added by alalme (Submitted the item)
  •  

    There are 0 votes so far. Votes easily highlight which items people would like to see resolved in priority, independently of the priority of the item set by tracker managers.

    Only logged-in users can vote.

     

    Follow 3 latest changes.

    Date Changed by Updated Field Previous Value => Replaced by
    2008-01-06 Beuc StatusNone Done
        Assigned toNone Beuc
        Open/ClosedOpen Closed

    Back to the top

    Powered by Savane 3.13-4448.
    Corresponding source code