cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
+
Summary of the contribution
+
Here is a numerical acount of the contribution's contents
+ and its timeline.
+
+
category
objects
propositions
theorems
39
lemmas
333
concepts
declared
33
defined
46
+
+ Support for abstract candidates of reducibility closed.
+
+
+ Confluence of context-sensitive parallel reduction closed.
+
+
+ Confluence of context-free parallel reduction closed.
+
+
+ Specification started.
+
Logical structure of the contribution
-
The source files are grouped in planes and components according to the following table.
-
component
plane
files
native typing
nty
conversion
context-sensitive
cpcs
computation
strongly normalizing
csn
context-sensitive
cprs
reduction
context-sensitive
lcpr
cpr
cpr_lift
cpr_tpss
cpr_cpr
context-free
ltpr
ltpr_drop
tpr
tpr_lift
tpr_tpss
tpr_tpr
static typing
atomic arity ass.
aaa
aaa_lift
aaa_aaa
static type ass.
sty
sty_lift
sty_sty
unfold
partial
ltpss
ltpss_drop
ltpss_tps
ltpss_ltpss
tpss
tpss_lift
tpss_tpss
tpss_ltps
substitution
parallel
ltps
ltps_drop
ltps_tps
ltps_ltps
tps
tps_lift
tps_tps
local env. dropping
drop
drop_drop
term relocation
lift
lift_lift
grammar
local env. ref. for substitution
lsubs
lsubs_lsubs
term hom.
thom
thom_thom
closures
cl_shift
cl_weight
internal syntax
lenv
lenv_weight
lenv_length
term
term_weight
term_simple
item
external syntax
aarity
parameters
sh
+
The source files are grouped in planes and components
+ according to the following table.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses.
+
+
component
plane
files
functional
reduction and type machine
rtm
rtm_step ( ? ⨠? )
unfold
lift ( â[?,?] ? )
subst ( [?â?] ? )
examples
native typing
nty
conversion
context-sensitive conversion
cpcs ( ? ⢠? â¬* ? )
computation
strongly normalizing computation
csn ( â¬* ? )
csn_cr
csn_aaa
context-sensitive computation
cprs (? ⢠? â¡* ?)
local env. ref. for abstract candidates of reducibility