From b4b18a8f2c3f33fe49edef3bc8068332edf299e2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 1 Jun 2016 14:33:30 +0000 Subject: [PATCH] - source web pages for lambdadelta_1 - minor bugs fixed in the web site --- .../lambdadelta_1/web/basic_1.ldw.xml | 46 ++++ .../lambdadelta_1/web/basic_1_blk.tbl | 39 ++++ .../lambdadelta_1/web/basic_1_src.tbl | 218 ++++++++++++++++++ .../lambdadelta_1/web/basic_1_sum.tbl | 28 +++ .../lambdadelta_1/web/ground_1.ldw.xml | 33 +++ .../lambdadelta_1/web/ground_1_src.tbl | 50 ++++ .../lambdadelta_1/web/ground_1_sum.tbl | 28 +++ helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_1.html | 2 +- helm/www/lambdadelta/basic_2.html | 2 +- helm/www/lambdadelta/documentation.html | 4 +- helm/www/lambdadelta/download/ld_talk_9s.pdf | Bin 67997 -> 67030 bytes helm/www/lambdadelta/ground_1.html | 2 +- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/implementation.html | 2 +- helm/www/lambdadelta/index.html | 6 +- helm/www/lambdadelta/news.html | 2 +- helm/www/lambdadelta/specification.html | 2 +- .../lambdadelta/web/home/documentation_2.tbl | 2 +- helm/www/lambdadelta/web/home/index.ldw.xml | 4 +- helm/www/lambdadelta/web/home/osn.ldw.xml | 6 +- 22 files changed, 462 insertions(+), 20 deletions(-) create mode 100644 helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml create mode 100644 helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl create mode 100644 helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl create mode 100644 helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl create mode 100644 helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml create mode 100644 helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl create mode 100644 helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml b/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml new file mode 100644 index 000000000..421276cf2 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml @@ -0,0 +1,46 @@ + + + + + + Abstract Syntax and Behavior + This is a summary of available syntactic items and reductions (block structure). + + + * In terms only. + + + Summary of the Specification + Here is a numerical account of the specification's contents + and its timeline. + +
+ + + Update with backports from the abandoned specification of λδ version 2. + + + Specification is concluded. + + + Decidability of native type assignment, λδ version 1 is released. + + + Preservation of native type by reduction, λδ version 1 is announced. + + + Specification starts. + + + Logical Structure of the Specification + This table reports the specification's components and their planes. + +
+ +
+ diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl new file mode 100644 index 000000000..996e35b50 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl @@ -0,0 +1,39 @@ +name "basic_1_blk" + +table { + class "gray" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "→ζ *" ] [ "annotator (with →ϵ *)" ] + [ "applicator (with →θ *)" ] [ "reference *" ] [ "reduction" ] + ] + } ] + [ { "{X | Γ ⊢ ⊤}" * } { + class "wine" [ + [ "exclusion" ] [ "Γ ⊢ χ" ] + [ "yes" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "magenta" [ + [ "typed abstraction" ] [ "Γ ⊢ λW" ] + [ "no" ] [ "<W>" ] [ "(V)" ] [ "#i" ] [ "→β *" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "prune" [ + [ "abbreviation" ] [ "Γ ⊢ δV" ] + [ "yes" ] [ "no" ] [ "no" ] [ "#i" ] [ "→δ" ] + ] + } ] + [ { "no" * } { + class "blue" [ + [ "sort" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "top" { * } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl new file mode 100644 index 000000000..6afa13d55 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl @@ -0,0 +1,218 @@ +name "basic_1_src" + +table uri "static/coq/lambdadelta/basic_1/" ext ".txt" { + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "wine" + [ { "examples" * } { + [ { "terms with special features" * } { + [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ] + } + ] + } + ] + class "magenta" + [ { "" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] +(* + [ { "higher order dynamic typing" * } { + [ { "higher order native type assignment" * } { + [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + } + ] + } + ] +*) + class "prune" + [ { "dynamic typing" * } { + [ { "well-formed contexts" * } { + [ @@"wf3_defs" @@"wf3_props" * ] + } + ] + [ { "context ref. for native type assignment" * } { + [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ] + } + ] + [ { "native type assignment" * } { + [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ] + } + ] + } + ] + class "blue" + [ { "equivalence" * } { + [ { "context-sensitive equivalence" * } { + [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ] + } + ] + [ { "context-free equivalence" * } { + [ @@"pc1_defs" @@"pc1_props" * ] + } + ] + } + ] + class "sky" + [ { "" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] + class "cyan" + [ { "computation" * } { + [ { "context ref. for reducibility" * } { + [ @@"csubc_defs" @@"csubc_props" * ] + } + ] + [ { "reducibility" * } { + [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ] + } + ] + [ { "strongly normalizing computation" * } { + [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ] + } + ] + [ { "context-sensitive computation" * } { + [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ] + } + ] + [ { "context-free computation" * } { + [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ] + } + ] + } + ] + class "water" + [ { "reduction" * } { + [ { "normal forms for context-sensitive reduction" * } { + [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ] + } + ] + [ { "context-sensitive reduction" * } { + [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ] + } + ] + [ { "normal forms for context-free reduction" * } { + [ "" @@"nf0_dec" * ] + } + ] + [ { "context-free reduction" * } { + [ @@"wcpr0_defs" * ] + [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ] + } + ] + } + ] + class "green" + [ { "unfold" * } { + [ { "iterated static type assignment" * } { + [ @@"sty1_defs" @@"sty1_props" * ] + } + ] + } + ] + class "grass" + [ { "static typing" * } { + [ { "static type assignment" * } { + [ @@"sty0_defs" @@"sty0_props" * ] + } + ] + [ { "context ref. for binary arity assignment" * } { + [ @@"csuba_defs" @@"csuba_props" * ] + } + ] + [ { "binary arity assignment" * } { + [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ] + } + ] + [ { "binary arity" * } { + [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ] + } + ] + [ { "parameters" * } { + [ @@"parameter_defs" * ] + } + ] + [ { "basic context ref." * } { + [ @@"csubv_defs" * ] + } + ] + } + ] + class "yellow" + [ { "multiple substitution" * } { + [ { "iterated context slicing" * } { + [ @@"drop1_defs" @@"drop1_props" * ] + } + ] + [ { "generic term relocation" * } { + [ @@"lift1_defs" @@"lift1_props" * ] + } + ] + } + ] + class "orange" + [ { "substitution" * } { + [ { "ordinary substitution" * } { + [ @@"subst_defs" @@"subst_props" * ] + [ @@"csubst1_defs" @@"csubst1_props" * ] + [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ] + } + ] + [ { "normal forms for ordinary strict substitution" * } { + [ "" @@"dnf_dec" * ] + } + ] + [ { "ordinary strict substitution" * } { + [ @@"fsubst0_defs" * ] + [ @@"csubst0_defs" * ] + [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ] + } + ] + [ { "basic local env. slicing" * } { + [ @@"getl_defs" @@"getl_props" * ] + [ @@"drop_defs" @@"drop_props" * ] + } + ] + [ { "basic term relocation" * } { + [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "closures" * } { + [ @@"flt_defs" * ] + } + ] + [ { "contexts" * } { + [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ] + } + ] + [ { "terms" * } { + [ @@"tlist_defs" * ] + [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ] + } + ] + } + ] +} + +class "top" { * } + +class "capitalize italic" { 0 } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl new file mode 100644 index 000000000..c87e8d037 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl @@ -0,0 +1,28 @@ +name "basic_1_sum" + +table { + class "gray" [ "category" + [ "objects" * ] + ] + class "cyan" [ "sizes" + [ "files" "120" ] + [ "characters" "198089" ] + [ "nodes" "1449099" ] + ] + class "green" [ "propositions" + [ "theorems" "81" ] + [ "lemmas" "618" ] + [ "total" "699" ] + ] + class "yellow" [ "concepts" + [ "declared" "39" ] + [ "defined" "47" ] + [ "total" "86" ] + ] +} + +class "capitalize italic" { 0 } + +class "italic" { 1 } { 3 } { 5 } + +class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml b/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml new file mode 100644 index 000000000..846fe7ce9 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml @@ -0,0 +1,33 @@ + + + + + + Summary of the Specification + Here is a numerical account of the specification's contents + and its timeline. + +
+ + + Update with backports from the abandoned specification of λδ version 2. + + + Specification is concluded. + + + Specification starts. + + + Logical Structure of the Specification + This table reports the specification's components and their planes. + +
+ +
+ diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl b/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl new file mode 100644 index 000000000..f8ce17263 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl @@ -0,0 +1,50 @@ +name "ground_1_src" + +table uri "static/coq/lambdadelta/ground_1/" ext ".txt" { + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "grass" + [ { "multiple relocation" * } { + [ { "" * } { + [ @@"bg_plist" * ] + } + ] + } + ] + class "yellow" + [ { "extensions to the library" * } { + [ { "" * } { + [ @@"bg_hints" @@"bg_blt" * ] + } + ] + } + ] + class "orange" + [ { "generated logical decomposables" * } { + [ { "" * } { + [ @@"bg_types" @@"bg_props" * ] + } + ] + } + ] + class "red" + [ { "preamble" * } { + [ { "" * } { + [ @@"bg_require" @@"bg_rewrite" @@"bg_tactics" @@"bg_subst" * ] + } + ] + } + ] +} + +class "top" { * } + +class "capitalize italic" { 0 } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl b/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl new file mode 100644 index 000000000..88451619c --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl @@ -0,0 +1,28 @@ +name "ground_1_sum" + +table { + class "gray" [ "category" + [ "objects" * ] + ] + class "cyan" [ "sizes" + [ "files" "10" ] + [ "characters" "15063" ] + [ "nodes" "14881" ] + ] + class "green" [ "propositions" + [ "theorems" "0" ] + [ "lemmas" "50" ] + [ "total" "50" ] + ] + class "yellow" [ "concepts" + [ "declared" "24" ] + [ "defined" "4" ] + [ "total" "28" ] + ] +} + +class "capitalize italic" { 0 } + +class "italic" { 1 } { 3 } { 5 } + +class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 602ed2c57..e4e4b3450 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 720fb0dee..9f7e234b6 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index f6b288778..78dd5c0f4 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Tue, 31 May 2016 21:18:48 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5c8b09d63..42152ed06 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -811,6 +811,6 @@

-
Last update: Tue, 31 May 2016 21:18:48 +0200
+
Last update: Wed, 01 Jun 2016 16:23:07 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 0fedfb151..a687f7a62 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -183,7 +183,7 @@
- +
P2d. F. Guidi: Considerations on Automath in Light of the Grundlagen (2016-05). Presentation at University of Bologna (slides).F. Guidi: Considerations on Automath in Light of the Grundlagen (revised 2016-06). Presentation at University of Bologna (slides).
@@ -401,6 +401,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/download/ld_talk_9s.pdf b/helm/www/lambdadelta/download/ld_talk_9s.pdf index 3f7c2bee7ab7591d8dcf4b255049bc8be9aab8c2..b7f3ca96cc3b04af78fb98e9cfb3b3327b3130e9 100644 GIT binary patch delta 11083 zcmb_iTWlQF8CC)avbg{aR{_l_VBs{f=XPdhmxf5bf=iq@>!b-7P{+Ho&X)DAvpY@# zQnfNF5ec$lGOc(jQY-bTFOA%XK88wFANoL5q)L4#s?t(beL+R)LtmiZe`aU)oS98_ z|@s=^!V>3ry9GgEdF*|GI>@7ng^wY}~y| zNA37GWE=TyEPQ2S7@zNKynxSZ8^aH)E7GwqJad_BJ?ymt@(?pjxLUQD(V}1`gdX}P z?R5zP95oZP74wWtE6TPSG{>aI(YaZM;lA4e-ud9g`M?W&xj{j$Uv!!1K<(0ysu0R{ zCn$4FGk5j*^V??#U#+0&d&^y@SyD5t=(ifHO#-?giZGLmf!TA-Mu~v4pn+N8f6ni1 z)11T{3sXLxKeqf;>Jm#ZEDZGpUD7i^a2ra~n{ z;eonv6WdZ;vYZZ=KE3+%o?6#HL*c$eCSbEerg*Uuj>WGWgkDCUxZ>Nnt0 z_|2^yE>G zFc&i_eDJ+z9{^>s2HoFq?7jWr@7Et8j)6Dtzvs5aw^qSG?BmSJ1J$+-)6`XwO~tIM z%?_VO031)TKr7XjtL+vCu8VVV1E0{BF(ys*`vlytqyjb=?Rc)?H5Y;Lb z5$Ux`jai&&r$o3fFV;lFPbC0WKw5|^)clH?5loqyDTk#qf>Y2rt>@;!-|l!q$_OT{ zO%gHUB!H-q!eqq1G}7of0{7(jskzxH0d6cp3~pY)f{1|KNh=YKpBb?%K-tz=f!oaG z1*|u96@_zQRx$Lh?Yl3|Dw~_v%xzOWpezMPLnO#JKgNNciB$yv5?C%@+#mjK{V@^c ze{*p({PN;c;nx>;h4)|D3q(G1$;Rg^mn?j)U!vIlhfAaF!N3TwNrAq@u5NN;!q*BG z6|YIQm`d~V zTLBU^;TH)8?Y#QZV$&26846J`jI0glHTC+bzGRsf=tlVh$>^bU`%KNG&Y zzBl>z%k^)BpRDhZlv1piD58J0{^X!+v1PjGcv7PaGb4E;h3-kkn-X6PSs7KeB1kXt z6|5@)^&&KgzilR*L4Ws!$UmER-F5W7>0W{eNn47vy%dqK z0#l16QMm0KYl}H;MGlFXqPPBX2x&-~nM#=L5o5ZXvrVC{H?M!RZ@WYoL=UNtL=6$> zBlbAR)ZKJZoH=>)#58zud`8+>IJT8ZJPFt}U#n^>*cdg+`=hSL+Z~lR0@=!Km!bUt zqDYK#BT-~n211maj)ZsM$3z%$v9%&yEYG2$9wT7Rd!FCBN#-# zmQLY7U7H(~`u~;xk5=F{-#LQ}wc}g_BEmcGrrM7a~LqhT)jsSP9EM$`A zue7SQMjaL2rf;ACv>J5NDF`RvUu#vDmhl(T&uUZ=s-9`3#xhDB)Q$3wg9O$Ju*rg! zgu3!nv1G~IPNk88kh+^Yf8=bF@(A|g5~Nkvr}Kzq8+nmO-u?L}yJcF);UeA^*k%Uh z{p8ijsoA+>uYxbLGGCA*fYgk>8d?~!j7VP@I$~csl?cO%lu8nT6@L7)Wo$Jvtca07 zKu}U*l0^hQfTeC05uQd#jCX7kq3J0;Z~)K3evFHt76IFKNyXA{_^)>#Oq5x?57#a{ zgnjuF;TsorAiJEt@EkrjE)2C9$0|qd;!oSAEs?rTH=>B4YBh2r^rxiNtj?iAmmWk>o89#D}Ad?t+tYs#6;0q|D?o~q@+02aQ$vdzZFj^2<~_?3qlO`I%G_i|}M1eGEE|PBIV%I@7|DXMr-Y#~O2-*w9!ql{j#RRv4 zVlnN(T&$v4-k_W9+ZRbre-yieqBw8axy_-mr*`%fOio`EJ00n$pjb?BD=rq(9>~S6 zisC!%Vz)nv-9b@Yz@~KbCx=VDUF`Nnu`o4_Vllxjxi}JG1H@wY#wgB@XRqVj{;15$ zs3gJJy+r|Oid`{P&!>Q^7?(peC zXOMbrysyEASIU*(O=gbj*gCOu=gy6af>E5!p*v*2@@ffUakv`z=Yx?IZ?)DKF`#{4 zi%L*=v{f0c`@u-9an4(+`qc8Z{re@;&o})_4mX8XPEUSt(rbSo2PhR56*}CZ<8Jz4 z^-fvzgo;u<-L>eDU9IQXn0&fSH{1{J-@fhHw(Zarvf4s7=oUdOb8K4EbQv8Ur^Wir`8upS7RnMu2d!FWAMX$*TaXhj)MuV>FeIOl0sJBFD7 zt78D_opIYS`car!C&ZMDs~w)FSGnRz2Tc#JUNm#!y}Oxur9rP0(b>H=GszYXdS2P~ z%XWq9r4j-^_YJ$SXql$r`+BLsjYIPXjdH1yH_KMZu^02GlF!?=pD&lWUbZSFzirp+eK+NoXAP>pwI?IG*k zWoMk&L1M%U7a^c954=!9dEtqNQXY_~#7iZFKmr~>;(?oliiD5=At6+t;{VUw&dlt( zPK=}2GiT2EFW-MT|GE6?3rAlFkAC>%^1@P;PHED~AN}Ra-;#7$k^37Tmu6XqC&Nl%uk-VbnlrG8QuZu zsFa!sAr(jE#ZghhNS@&*-zJp_@eZ7juBU`pSt6E6^x9{hA3=zB;DiiIOC(~ol0?i( zC91!8brd1&5E0U7LP#qktz}R@^qpfP2=NY)YGw+yu9PIwX)4i+-~aUpLc9YfWEv?( zdRZbpljt9>zW@F**t`QLRAYLgno*X>$RzswFIpoA@eZ7jrDTN45*e99+Hb#iq+aqP z-T?_|s*wm}mIX31fu8xp#Rtlo@eW9bF)Jff7Rby5I{mlc{^^oHyhEfJV~Iq9U$5>B z9I|Y0I^pI2Oq_tHq0{qa^w*|DnvU1s8MYh`;&FM{Z>>0fIQ9F9C5jrs_oY7crCb-O zUYE!`yu)x$MnRj{6h|plp#h};LU+vZ@Bfz1sS%Tiql(lx`HUkEdXc3n#N1u6WTKL6 zgpxcxh%DJ*wPX=)k(P{`HjgV$BsrGmA%WE*EF+d$WcQpYdCC!4YKQS2w55hJC*GrB zM&sl&Tk_Y|qV2rYTS%dtGHmWHUMF+xk88by}I zVYGxyaLy35G)8D?6jOn5SS?LaOLK&lJl~31nupO6JT@>zEzJ>Hnnf*9tSH~fJmJYa z$9gh(%58h{RS6|(N<1w#C7!C95>FrSCt}9KtSM;#R{&kPKf)hGuPJf6!Jp`j>(`X7 z$q+(2n2}X6^`?@mkemm_n1UHHo8`edP&0`C1qoKv{-HPd-yiqFi&*gkp_y zKJchZl$(JxOVoKTPlgw$!yGG0rq(2t%SM_og{zo^gCaRE%O}bisdjLYprMYOD#N}V)kck&%v6QEH~zw z&9jfsH&$1v%4@3y$7>DUf!`m>8m}dJE)D57A3jDd*q%SXWe*{7Q?ll^{VngR96olt zazqN7w;w+$=~N3}dgKG}`swPi@Z-0oqY%VW`08yPnqI$sB3SIT`fazjDc5+>NLF?> zd@Ss-@P+)Gl;QkqEGw^xlW_zkPhZyD-dxXf)At3p({W&301JVu60^uBcKW_EbT_yB zYZ2`LY4WUD1fqF1Mm*mhN){y@Fl6klXeeGkL>4>7ou7wo^UCGLD;L3JO{#<+ zyLfCWDtLbfo<3?%X) zHwJ26>l7Vr;q3ZyW06a37IO`aEO&ZjjOE-)P1KOXuV2W7f9(P}DrtHxd}rfiSZ|;+ zH5-_AKG$II`<2El{C>SLC8VGzs>f(h!>_Rhci}9NuaE_F4vB#oxHsrzIdCO#p-zW% zT(Gsov?xopH@ZAg<c~+9|V(B*H6OlkF0+P zeka-BcmSbM40Uuy_%Ar4%+o=0+$6%k-kk-5bQS>>Hg>vQ$A|KrIG@;YZ`fU&U?fOy zUB~mF$p$MjVh@M?n~@1MND=s!+ElZM+v~VJ*WZKn5$QRbw(s_PJod@9J@EWK+3C4A zoS_HAEQ7q$-x>Bi-|aeRby%-x;oH}a2SQ#DQdv5gUp{~F+}sKn?(BMb4%=r6gU%yo zc7yK`gP+CISoqoMd%#LRe*`l3S107~9TWG4^2Ghnbb6u&znzIm`2D2`jI^IlOlFa0 z@s;pcI|+514qP-0pjHP<$?AiYA)hd;%DpUb5 z8_BTCeGRAEP1rq@$eh>0eMsE;CiC{-2?wi<==DitfFE(FM9#x%)@{x8HoFcWN>+Sl z`)S!Ufy9kXUP~c$i8Sn8@y+!-D3`)NeB+UO36@^Cv-#r}zP83ihPZc_Y;x0P%JTQI znE^P9HP?JvEf@wAU@!mat2d-HJ@C5cAh4CICk~q;S7E8G!48w5vjjBCDEM=RoX&E{ z!D|3%Ge(XAQX_#gY5-LPP7D{M6tW)UufYLA0@oyQh)V`g2lm^i1lVerK!x=Rf9J~5 z8L01yRn<7$bkzXZPPUHUlffpGXX$)4%G=77SLAK5&abMl(?=DU7EN7ApvzE$MiDjs z8vg6)2iZulsIHDeEAgjK?QVM6sfr=jU<=)(Mgj^0-Qp;O)*LGM3b;QNN1+0*qw!I}UH0)N?xJzN8Z>f7;h)7D{DH>NF5a7Hm@< zIFi6;!hb(~|J@)HKDhS9958$XRRBiV;yt*3P{vdM=E&v6x1_)n>(g;lTDdBS`~#L_ zRaK#IECwgDrjjNZ2$Ce6Fr{Xb8uWp1Y9y%{#*Pao4d=1($yvuJjl-#V?AtlG_{OLJ zm#{Z^aJY00!|A109(#9&mf(=wjgo!jEU&LOE+ms7Wi`M%uA67h><;YKb;p-CoK3ek zTlwn`epr#+_H1QMZzzqyytCy#ack(T+`72hx^=x}wJT@p(##nf_L>8yx@!-r9X_3S zGGI4*V!nA{=>+!Jo!;FZY{Pm{-rer@yy@N93XXB6;TfArMdn@n>$8>h#C;+s|x&7?HYB|wrOtAwwmx8v@=T}QXw$_f>^;Axeg{4m}fK&VAB|g8R#?JfIY3w z-U95v)FCR2s-jm_W0mUDN}x>Z`s0c^ttd03&=nj2#?Hef5!ksIF}65V=qU{C4_Co0 z>g^luz?-~&O4g?=I2oDm5B6{|5`ecTFkd$9w%fA1^5UK&uk<_qO*lS}1maX(qIK z&UO9hq3a@#>8{<|oUQCu+fK*c>H3v=xBVQf7Op>Mc~fB6$ShsA9zF2UB%?UOXuJvX zKs}Ja%1N53OY;Be=fH%5H)9BSGRdw`B+gcDV(x^e{N*X3s7i9c67Tz~}nuH4V2Kb8RpdZ#@*-@LW09rdlQ!K7iI#dPOmDw>j5QQ7znY%C$l1 zi|1vzHr;^rVxf)c3NA!){a`;BkDZe?e^OyISXvj`7_BKI+VC1lZmeoq zN>Lb41aH0M`YC##<0XPzBh%ohq|gRUxUrJ&$Fy1z1x;bNl+X907L;tIHar+sV6w?H zhT{i3d(RC9|Hp%sd>dRyD>7ynGlhQ8hS%zHW0{gyB*MSO@c1m(5f=O<#tbAZIjgDS z#i86-rczus7TfS1OukKFL5T?k&P67anRu@+KUh`qN>j0|Y)(bT1La&lpogc4@B`Nm zlGvrNn^I;1K3o{gREGNwIf4wrxafpH4{u%M`cX^AJC#`*;?GpAEVZgxCGEf>xxp|N z2;#+?j37LLh4G$8u8paBS!l?xpnstwRq#SXZZHtU)98E~Q}Bjlu8pZiS!mTPM-HX6 z*k^(ieibk*5>yQxuc{Q7n0OJg*k+a5C@YNxdIh8bf5^pntEWJ)R?1uqGGWO-Orzxe zngSD7fu2Tnym*%5q3N2zf?}g(lyU%wrxYDYuho>IFEF^zSyF_VCI4W+IT?Fj;{7cA z${P;{OgHhmQBF=~Xm~V~Z!>8r_+T~^t?v(Q*y8u3?`jCxp-+w`X52a#h(BG diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index bf75563e5..1362fd68a 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Tue, 31 May 2016 21:18:48 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index fc266948a..d982e3846 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -823,6 +823,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 6bf8c301f..6c8adae77 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index b3e330c9f..ea9e12c41 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -186,7 +186,7 @@
Disclaimer [spacer]
- The systens of the λδ family are not related intentionally to + The systems of the λδ family are not related intentionally to any other system having (variations of) the symbols λ and δ in its name or syntax. Examples include (but are not limited to):
@@ -252,7 +252,7 @@
[Smiling face] - Moreover, the systens of the λδ family are not related intentionally to + Moreover, the systems of the λδ family are not related intentionally to Lady Lambdadelta, the Witch of Certainty of the sound novel Umineko no Naku Koro ni. @@ -283,6 +283,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 6101558d2..80e936a07 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index ec0d85773..f67b59787 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 3e59b57e6..7b450ff46 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -48,7 +48,7 @@ table { "F. Guidi:" + @@("download/ld_talk_9s.pdf" "Considerations on Automath in Light of the Grundlagen") + - "(2016-05)." + + "(revised 2016-06)." + "Presentation at University of Bologna (slides)." * } ] diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index c5004f36a..a7e9b6702 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -86,7 +86,7 @@ Disclaimer - The systens of the λδ family related intentionally to + The systems of the λδ family related intentionally to any other system having (variations of) the symbols λ and δ in its name or syntax. Examples include (but are not limited to): @@ -146,7 +146,7 @@ - Moreover, the systens of the λδ family related intentionally to + Moreover, the systems of the λδ family related intentionally to Lady Lambdadelta, the Witch of Certainty of the sound novel Umineko no Naku Koro ni. diff --git a/helm/www/lambdadelta/web/home/osn.ldw.xml b/helm/www/lambdadelta/web/home/osn.ldw.xml index ef8580bb8..d83efaaaf 100644 --- a/helm/www/lambdadelta/web/home/osn.ldw.xml +++ b/helm/www/lambdadelta/web/home/osn.ldw.xml @@ -11,7 +11,7 @@ is an easy and flexible data-interchange text format intended for the lightweight representation of generic abstract syntax trees in the domain of formal systems. - In order to meet theese design goals, OSN pursues the following features. + In order to meet these design goals, OSN pursues the following features. -- 2.39.2