[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Savannah-register-public] [task #5045] Submission of Separation Logic i
From: |
Reynald Affeldt |
Subject: |
[Savannah-register-public] [task #5045] Submission of Separation Logic in Coq |
Date: |
Thu, 15 Dec 2005 02:00:41 +0000 |
User-agent: |
Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.10) Gecko/20050925 Firefox/1.0.4 (Debian package 1.0.4-2sarge5) |
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/
- [Savannah-register-public] [task #5045] Submission of Separation Logic in Coq,
Reynald Affeldt <=