helm/coq-contribs/SUBSETS/README

   1
   2                           Contribution  Padova/SUBSETS
   3                           ============================
   4
   5 This directory contains a formalization in Coq of the content of this paper
   6 describing a theory of subsets on a intuitionistic a predicative foundation:
   7
   8 G.Sambin, S.Valentini:
   9 Building up a toolbox for Martin-Lof's type theory: subset theory.
  10 In Proc. of Twenty-five years of constructive type theory,
  11 Oxford U.P. (1998) pp. 221-244.
  12
  13 Author & Date: Ferruccio Guidi
  14                Department of Computer Science, University of Bologna
  15                March 2005
  16 E-mail : fguidi@cs.unibo.it
  17 WWW    : http://www.cs.unibo.it/~fguidi
  18
  19 Installation procedure:
  20 -----------------------
  21
  22   To get this contribution compiled, type
  23
  24     make
  25
  26   or
  27
  28     make opt
  29
  30   The main modules produced by the compilation are:
  31
  32      Toolbox   provides the theory of subsets and its prerequisites
  33
  34      Base      provides just the prerequisites
  35
  36 Description:
  37 ------------
  38
  39 Further information on this contribution:
  40 -----------------------------------------
  41
  42   The latest version of this development is maintained in the CVS repository
  43   of the HELM project <helm.cs.unibo.it> and can be downloaded at:
  44
  45   www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz