helm/software/components/ng_kernel/paper.txt

   1 A compact kernel for the calculus of inductive constructions
   2
   3 descrizione di CIC (17pp) Andrea
   4    105 nCic.ml
   5    106 nCicUtils.ml
   6    134 nReference.ml (Pp usa environment, spostare nomi in ref?)
   7   - descrizione pragmatica di CIC (3pp)
   8   - motivare scelte (cosa era costoso)
   9   - confronto con il vecchio (sia calcolo che implementazione)
  10   - descrizione ADT
  11   - iteratore (lift?)
  12   - self reference e debruijnate
  13   - locally nameless
  14   - sections (costi benefici, dentro/fuori kernel)
  15   - modules
  16
  17 descrizione environment(2pp) CSC
  18   93 nCicEnvironment.ml
  19   - frozen e ciclicità
  20   - trust, libreria -vs- env
  21
  22 descrizione di Subst (1pp)
  23   96 nCicSubstitution.ml
  24   - fattorizzazione di 3 subst
  25     - subst, e psubst (per unwind e kernel)
  26     - subst meta (con parametro per non liftare)
  27
  28 descrizione riduzione(8pp) Gares
  29    599 nCicReduction.ml
  30    - macchinine
  31      - strategia doppia
  32    - conversion
  33      - su macchine
  34      - height of objects (todo)
  35      - irrelevance (fare il checking che gli irrelev dichiarati siano irrel)
  36    - asymmetric convertion
  37
  38 descrizione type_checker(15pp) Wilmer(guardia)
  39   1183 nCicTypeChecker.ml
  40     - ricorsione guardata
  41     - positività
  42     - proof irrelevance
  43     - metasenv consistency
  44     - tensione tra typechecking di termini aperti e
  45       chi se ne frega, qed lavora su termini chiusi
  46     - universi, check contro inferenza
  47
  48 testing/conclusioni?
  49   - conversione old/new e problematiche
  50
  51 biblio
  52   - crafting, matita JAR
  53   - barthe, gregoire 5k
  54   - pollack, harper syntax directed rules
  55   - CIC... chrinstine, coquand, benjamin
  56   - jojgov, munoz, strecker Metas
  57   -
  58
  59
  60 appendice
  61
  62   nCicEnvironment.mli:val get_checked_obj: NUri.uri -> NCic.obj
  63   nCicEnvironment.mli:val get_obj: NUri.uri -> bool * NCic.obj
  64   nCicEnvironment.mli:val add_obj: NCic.obj -> unit
  65   nCicEnvironment.mli:val get_checked_def:
  66   nCicEnvironment.mli:val get_checked_indtys:
  67   nCicEnvironment.mli:val get_checked_fixes:
  68   nCicEnvironment.mli:val get_checked_cofixes:
  69   nCicEnvironment.mli:val get_indty_leftno: NReference.reference -> int
  70   nCicPp.mli:val ppterm:
  71   nCicPp.mli:val ppobj: NCic.obj -> string
  72   nCicReduction.mli:val whd :
  73   nCicReduction.mli:val are_convertible :
  74   nCicReduction.mli:val head_beta_reduce: ?delta:int -> ?upto:int -> NCic.term -> NCic.term
  75   nCicSubstitution.mli:val lift : ?from:int -> int -> NCic.term -> NCic.term
  76   nCicSubstitution.mli:val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
  77   nCicSubstitution.mli:val psubst :
  78   nCicSubstitution.mli:val subst_meta : NCic.local_context -> NCic.term -> NCic.term
  79   nCicTypeChecker.mli:val typecheck_obj : NCic.obj -> unit
  80   nCicTypeChecker.mli:val typeof:
  81   nCicUtils.mli:val sharing_map: ('a -> 'a) -> 'a list -> 'a list
  82   nCicUtils.mli:val expand_local_context : NCic.lc_kind -> NCic.term list
  83   nCicUtils.mli:val lookup_subst: int ->  NCic.substitution -> NCic.subst_entry
  84   nCicUtils.mli:val lookup_meta: int ->  NCic.metasenv -> NCic.conjecture
  85   nCicUtils.mli:val fold:
  86   nCicUtils.mli:val map:
  87   nCicUtils.mli:val is_closed: NCic.term -> bool
  88   nReference.mli:val eq: reference -> reference -> bool
  89   nReference.mli:val string_of_reference: reference -> string
  90   nUri.mli:val string_of_uri: uri -> string
  91   nUri.mli:val uri_of_string: string -> uri
  92   nUri.mli:val eq: uri -> uri -> bool
  93
  94 dimensione
  95
  96    vecchio:
  97    244 cic.ml
  98    459 cicEnvironment.ml
  99     62 cicLogger.ml
 100    534 cicPp.ml
 101   1244 cicReduction.ml
 102    451 cicSubstitution.ml
 103   2101 cicTypeChecker.ml
 104    147 cicUnivUtils.ml
 105    934 cicUniv.ml
 106     66 cicUtil.ml
 107    245 uriManager.ml
 108    =====
 109   6487
 110
 111    809 ../cic/cicParser.ml
 112
 113   nuovo:
 114    105 nCic.ml
 115    134 nReference.ml
 116    106 nCicUtils.ml
 117     93 nCicEnvironment.ml
 118    599 nCicReduction.ml
 119     96 nCicSubstitution.ml
 120   1183 nCicTypeChecker.ml
 121    173 nCicPp.ml
 122     41 nUri.ml
 123     =====
 124   2530
 125
 126