a contribution about subset theory in an intuitionistic and predicative foundation

[helm.git] / helm / coq-contribs / SUBSETS / README

diff --git a/helm/coq-contribs/SUBSETS/README b/helm/coq-contribs/SUBSETS/README
new file mode 100644 (file)
index 0000000..caf3735
--- /dev/null
+++ b/helm/coq-contribs/SUBSETS/README
@@ -0,0 +1,45 @@
+
+                          Contribution  Padova/SUBSETS
+                          ============================
+
+This directory contains a formalization in Coq of the content of this paper
+describing a theory of subsets on a intuitionistic a predicative foundation:
+
+G.Sambin, S.Valentini: 
+Building up a toolbox for Martin-Lof's type theory: subset theory.
+In Proc. of Twenty-five years of constructive type theory,
+Oxford U.P. (1998) pp. 221-244.
+
+Author & Date: Ferruccio Guidi
+               Department of Computer Science, University of Bologna
+               March 2005
+E-mail : fguidi@cs.unibo.it
+WWW    : http://www.cs.unibo.it/~fguidi
+
+Installation procedure:
+-----------------------
+
+  To get this contribution compiled, type
+
+    make 
+
+  or
+
+    make opt
+
+  The main modules produced by the compilation are:
+
+     Toolbox   provides the theory of subsets and its prerequisites
+
+     Base      provides just the prerequisites
+
+Description:
+------------
+
+Further information on this contribution:
+-----------------------------------------
+
+  The latest version of this development is maintained in the CVS repository
+  of the HELM project <helm.cs.unibo.it> and can be downloaded at: 
+   
+  www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz