[Savannah-register-public] [task #5045] Submission of Separation Logic in Coq

[Reynald Affeldt]

URL:
  <http://savannah.gnu.org/task/?func=detailitem&item_id=5045>

                 Summary: Submission of Separation Logic in Coq
                 Project: Savannah Administration
            Submitted by: reynald
            Submitted on: Thu 12/15/05 at 02:00
         Should Start On: Thu 12/15/05 at 00:00
   Should be Finished on: Sun 12/25/05 at 00:00
                Category: Project Approval
                Priority: 5 - Normal
                  Status: None
                 Privacy: Public
             Assigned to: None
        Percent Complete: 0%
             Open/Closed: Open
                  Effort: 0.00

    _______________________________________________________

Details:

A new project has been registered at Savannah 
The project account will remain inactive until a site admin approve or
discard 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):

  <https://savannah.gnu.org/admin/groupedit.php?group_id=8196>


######### REGISTRATION DETAILS ######### 

Full Name:
----------
  Separation Logic in Coq

System Group Name:
-----------------
  seplog

Type:
-----
  non-GNU software & documentation

License:
-------- 
  GNU General Public License V2 or later

Description:
------------
  Seplog is an implementation of separation logic (an extension of Hoare
logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the
Coq proof assistant (version 8, http://coq.inria.fr) together with a
sample verification of the heap manager of the Topsy operating system
(version 2, http://www.topsy.net). More information is available at
http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog.








    _______________________________________________________

Reply to this item at:

  <http://savannah.gnu.org/task/?func=detailitem&item_id=5045>

_______________________________________________
  Message sent via/by Savannah
  http://savannah.gnu.org/