--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ logo = "crux"
+ head = "cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)"
+>
+ <sitemap name="sitemap"/>
+
+ <section6 name="blocks">Abstract Syntax and Behavior</section6>
+ <body>This is a summary of available syntactic items and reductions (block structure).
+ </body>
+ <table name="basic_1_blk"/>
+ <body>* In terms only.
+ </body>
+
+ <section6 name="summary">Summary of the Specification</section6>
+ <body>Here is a numerical account of the specification's contents
+ and its timeline.
+ </body>
+ <table name="basic_1_sum"/>
+
+ <news class="delta" date="November 2019.">
+ λδ-1A is repackaged (was λδ-1).
+ </news>
+ <news class="delta" date="January 2015.">
+ λδ-1A is updated with backports from the abandoned specification of λδ-2.
+ </news>
+ <news class="delta" date="May 2008.">
+ λδ-1A is concluded.
+ </news>
+ <news class="gamma" date="November 2006.">
+ Decidability of native type assignment, λδ-1A is released.
+ </news>
+ <news class="beta" date="December 2005.">
+ Preservation of native type by reduction, λδ-1A is announced.
+ </news>
+ <news class="alpha" date="May 2004.">
+ λδ-1 started.
+ </news>
+
+ <section6 name="structure">Logical Structure of the Specification</section6>
+ <body>This table reports the specification's components and their planes.
+ </body>
+ <table name="basic_1_src"/>
+
+ <footer/>
+</page>
--- /dev/null
+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 }
--- /dev/null
+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 }
--- /dev/null
+name "basic_1_sum"
+
+table {
+ class "gray" [ "category"
+ [ "objects" * ]
+ ]
+ class "water" [ "sizes"
+ [ "files" "120" ]
+ [ "characters" "198089" ]
+ [ "nodes" "1449099" ]
+ ]
+ class "green" [ "propositions"
+ [ "theorems" "81" ]
+ [ "lemmas" "618" ]
+ [ "total" "699" ]
+ ]
+ class "grass" [ "concepts"
+ [ "declared" "39" ]
+ [ "defined" "47" ]
+ [ "total" "86" ]
+ ]
+}
+
+class "capitalize italic" { 0 }
+
+class "italic" { 1 } { 3 } { 5 }
+
+class "right italic" { 2 } { 4 } { 6 }
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ logo = "crux"
+ head = "cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)"
+>
+ <sitemap name="sitemap"/>
+
+ <section6 name="summary">Summary of the Specification</section6>
+ <body>Here is a numerical account of the specification's contents
+ and its timeline.
+ </body>
+ <table name="ground_1_sum"/>
+
+ <news class="delta" date="January 2015.">
+ Update with backports from the abandoned specification of λδ version 2.
+ </news>
+ <news class="delta" date="May 2008.">
+ Specification is concluded.
+ </news>
+ <news class="alpha" date="May 2004.">
+ Specification starts.
+ </news>
+
+ <section6 name="structure">Logical Structure of the Specification</section6>
+ <body>This table reports the specification's components and their planes.
+ </body>
+ <table name="ground_1_src"/>
+
+ <footer/>
+</page>
--- /dev/null
+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 }
--- /dev/null
+name "ground_1_sum"
+
+table {
+ class "gray" [ "category"
+ [ "objects" * ]
+ ]
+ class "water" [ "sizes"
+ [ "files" "10" ]
+ [ "characters" "15063" ]
+ [ "nodes" "14881" ]
+ ]
+ class "green" [ "propositions"
+ [ "theorems" "0" ]
+ [ "lemmas" "50" ]
+ [ "total" "50" ]
+ ]
+ class "grass" [ "concepts"
+ [ "declared" "24" ]
+ [ "defined" "4" ]
+ [ "total" "28" ]
+ ]
+}
+
+class "capitalize italic" { 0 }
+
+class "italic" { 1 } { 3 } { 5 }
+
+class "right italic" { 2 } { 4 } { 6 }
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
- description = "\lambda\delta home page"
- title = "\lambda\delta home page"
- logo = "crux"
- head = "cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)"
->
- <sitemap name="sitemap"/>
-
- <section6 name="blocks">Abstract Syntax and Behavior</section6>
- <body>This is a summary of available syntactic items and reductions (block structure).
- </body>
- <table name="basic_1_blk"/>
- <body>* In terms only.
- </body>
-
- <section6 name="summary">Summary of the Specification</section6>
- <body>Here is a numerical account of the specification's contents
- and its timeline.
- </body>
- <table name="basic_1_sum"/>
-
- <news class="delta" date="January 2015.">
- Update with backports from the abandoned specification of λδ version 2.
- </news>
- <news class="delta" date="May 2008.">
- Specification is concluded.
- </news>
- <news class="gamma" date="November 2006.">
- Decidability of native type assignment, λδ version 1 is released.
- </news>
- <news class="beta" date="December 2005.">
- Preservation of native type by reduction, λδ version 1 is announced.
- </news>
- <news class="alpha" date="May 2004.">
- Specification starts.
- </news>
-
- <section6 name="structure">Logical Structure of the Specification</section6>
- <body>This table reports the specification's components and their planes.
- </body>
- <table name="basic_1_src"/>
-
- <footer/>
-</page>
+++ /dev/null
-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 }
+++ /dev/null
-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 }
+++ /dev/null
-name "basic_1_sum"
-
-table {
- class "gray" [ "category"
- [ "objects" * ]
- ]
- class "water" [ "sizes"
- [ "files" "120" ]
- [ "characters" "198089" ]
- [ "nodes" "1449099" ]
- ]
- class "green" [ "propositions"
- [ "theorems" "81" ]
- [ "lemmas" "618" ]
- [ "total" "699" ]
- ]
- class "grass" [ "concepts"
- [ "declared" "39" ]
- [ "defined" "47" ]
- [ "total" "86" ]
- ]
-}
-
-class "capitalize italic" { 0 }
-
-class "italic" { 1 } { 3 } { 5 }
-
-class "right italic" { 2 } { 4 } { 6 }
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
- description = "\lambda\delta home page"
- title = "\lambda\delta home page"
- logo = "crux"
- head = "cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)"
->
- <sitemap name="sitemap"/>
-
- <section6 name="summary">Summary of the Specification</section6>
- <body>Here is a numerical account of the specification's contents
- and its timeline.
- </body>
- <table name="ground_1_sum"/>
-
- <news class="delta" date="January 2015.">
- Update with backports from the abandoned specification of λδ version 2.
- </news>
- <news class="delta" date="May 2008.">
- Specification is concluded.
- </news>
- <news class="alpha" date="May 2004.">
- Specification starts.
- </news>
-
- <section6 name="structure">Logical Structure of the Specification</section6>
- <body>This table reports the specification's components and their planes.
- </body>
- <table name="ground_1_src"/>
-
- <footer/>
-</page>
+++ /dev/null
-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 }
+++ /dev/null
-name "ground_1_sum"
-
-table {
- class "gray" [ "category"
- [ "objects" * ]
- ]
- class "water" [ "sizes"
- [ "files" "10" ]
- [ "characters" "15063" ]
- [ "nodes" "14881" ]
- ]
- class "green" [ "propositions"
- [ "theorems" "0" ]
- [ "lemmas" "50" ]
- [ "total" "50" ]
- ]
- class "grass" [ "concepts"
- [ "declared" "24" ]
- [ "defined" "4" ]
- [ "total" "28" ]
- ]
-}
-
-class "capitalize italic" { 0 }
-
-class "italic" { 1 } { 3 } { 5 }
-
-class "right italic" { 2 } { 4 } { 6 }
% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@comment{lambdadeltaJ2a,
+@comment{lambdadeltaR2d,
author="Ferruccio {Guidi}",
- title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}",
+ title="{Two Formal Systems of the $\lambda\delta$ Family Revised}",
howpublished="CoRR identifier 1411.0154",
year="2014",
month="November",
note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
}
+@misc{lambdadeltaV2b,
+ author="Ferruccio {Guidi}",
+ title="{lambdadelta\_2B}",
+ howpublished="Formal specification for the interactive prover Matita 0.99.4",
+ year="2019",
+ month="November",
+ note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$"
+}
+
@techreport{lambdadeltaR2c,
author="Ferruccio {Guidi}",
title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}",
@misc{lambdadeltaV2a,
author="Ferruccio {Guidi}",
- title="{lambdadelta\_2A1}",
- howpublished="Formal specification for the proof assistant Matita 0.99.2",
+ title="{lambdadelta\_2A}",
+ howpublished="Formal specification for the interactive prover Matita 0.99.2",
year="2014",
month="October",
note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$"
@misc{lambdadeltaV1a,
author="Ferruccio {Guidi}",
- title="{lambdadelta\_1}",
- howpublished="Formal specification for the proof assistant Coq 7.3.1",
+ title="{lambdadelta\_1A}",
+ howpublished="Formal specification for the interactive prover Coq 7.3.1",
year="2006",
month="November",
note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$"
% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@comment{lambdadeltaJ2a,
+@comment{lambdadeltaR2d,
author="Ferruccio {Guidi}",
- title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}",
+ title="{Two Formal Systems of the $\lambda\delta$ Family Revised}",
howpublished="CoRR identifier 1411.0154",
year="2014",
month="November",
note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
}
+@misc{lambdadeltaV2b,
+ author="Ferruccio {Guidi}",
+ title="{lambdadelta\_2B}",
+ howpublished="Formal specification for the interactive prover Matita 0.99.4",
+ year="2019",
+ month="November",
+ note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$"
+}
+
@techreport{lambdadeltaR2c,
author="Ferruccio {Guidi}",
title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}",
@misc{lambdadeltaV2a,
author="Ferruccio {Guidi}",
- title="{lambdadelta\_2A1}",
- howpublished="Formal specification for the proof assistant Matita 0.99.2",
+ title="{lambdadelta\_2A}",
+ howpublished="Formal specification for the interactive prover Matita 0.99.2",
year="2014",
month="October",
note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$"
@misc{lambdadeltaV1a,
author="Ferruccio {Guidi}",
- title="{lambdadelta\_1}",
- howpublished="Formal specification for the proof assistant Coq 7.3.1",
+ title="{lambdadelta\_1A}",
+ howpublished="Formal specification for the interactive prover Coq 7.3.1",
year="2006",
month="November",
note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$"
]
[ { name "ldV1a" "<span class=\"emph alpha\">V1a.</span>" "" } {
"F. Guidi:" +
- @@("html/version_1.html" "lambdadelta_1") +
- "(revised <span class=\"emph delta\">2015-01</span>)." +
+ @@("html/version_1.html" "lambdadelta_1A") +
+ "(revised <span class=\"emph delta\">2019-11</span>)." +
"Formal specification for the proof assistant Coq 7.3.1 (scripts)." +
@@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
[ { name "ldV2a" "<span class=\"emph alpha\">V2a.</span>" "" } {
"F. Guidi:" +
- @@("html/version_2.html" "lambdadelta_2A1") +
- "(revised <span class=\"emph gamma\">2014-10</span>)." +
+ @@("html/version_2.html" "lambdadelta_2A") +
+ "(revised <span class=\"emph delta\">2019-11</span>)." +
"Formal specification for the proof assistant Matita 0.99.2 (scripts)." +
@@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
* }
<section3 name="milestones">Milestones</section3>
+ <news class="delta" date="November 2019.">
+ The specifications of λδ-1A and λδ-2A are repackaged
+ (they were λδ-1 and λδ-2A1 respectively).
+ </news>
+
<news class="gamma" date="November 2019.">
The specification of
- <rlink to="html/documentation.html#ldV2b">λδ-2B</rlink>
+ <rlink to="html/specification.html#source2B">λδ-2B</rlink>
is released.
</news>
+ <news class="beta" date="November 2018.">
+ The specification of
+ <rlink to="html/documentation.html#ldP2e">λδ-2B</rlink>
+ is announced.
+ </news>
+
<news class="alpha" date="December 2015.">
<rlink to="html/documentation.html#ldJ3a">Second journal paper on λδ</rlink>
accepted for publication.
<rlink to="html/implementation.html#v3">"Helena 0.8.3"</rlink> is released.
</news>
+ <news class="alpha" date="October 2015.">
+ The specification of λδ-2B is started.
+ </news>
+
<news class="delta" date="August 2015.">
The specification of λδ-2A is concluded.
</news>
<news class="gamma" date="October 2014.">
The specification of
- <rlink to="html/documentation.html#ldR2c">λδ-2A</rlink>
+ <rlink to="html/specification.html#source2A">λδ-2A</rlink>
is released.
</news>
</news>
<news class="beta" date="June 2014.">
- <rlink to="html/documentation.html#ldP2c">First communication on λδ-2.</rlink>
+ The specification of
+ <rlink to="html/documentation.html#ldP2c">λδ-2A</rlink>
+ is announced.
</news>
<news class="alpha" date="December 2012.">
</news>
<news class="delta" date="June 2008.">
- The <rlink to="html/specification.html#static1">
+ The <rlink to="html/specification.html#static1A">
HTML pages of the specification of λδ-1A for Matita 0.5</rlink>
are online.
</news>
</news>
<news class="gamma" date="September 2007.">
- The <rlink to="html/specification.html#dynamic1">
+ The <rlink to="html/specification.html#dynamic1A">
specification of λδ-1A for Matita 0.4</rlink>
is online.
</news>
<news class="gamma" date="November 2006.">
The specification of
- <rlink to="html/documentation.html#ldR1b">λδ-1A</rlink>
+ <rlink to="html/specification.html#source1A">λδ-1A</rlink>
is released.
</news>
<news class="beta" date="December 2005.">
- <rlink to="html/documentation.html#ldP1a">First communication on λδ-1</rlink>.
+ The specification of
+ <rlink to="html/documentation.html#ldP1a">λδ-1A</rlink>
+ is announced.
</news>
<news class="alpha" date="May 2004.">
<section3 name="visibility">Visibility</section3>
- <news class="alpha" date="June 2014.">
+ <news class="alpha" date="November 2019.">
The <link to="http://www.google.com/">Google</link>
search for "formal system lambda delta" gives
- 5 resources about the λδ family in the first 6 results.
+ 9 resources about the λδ family in the first 10 results.
</news>
- <news class="alpha" date="June 2014.">
+ <news class="alpha" date="November 2019.">
The <link to="http://www.yahoo.com/">Yahoo</link>
search for "formal system lambda delta" gives
- 4 resources about the λδ family in the first 5 results.
+ 14 resources about the λδ family in the first 14 results.
</news>
<footer/>
<subsection name="v2"><img logo="ld2"/>λδ version 2 (active)</subsection>
<body>
The formal specification of λδ version 2
- is available in the following formats:
+ is available in the following formats.
</body>
- <topitem name="source2">
- <body>
- <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
- (revised <notice class="gamma" text="2014-10"/>).
- Source scripts [Svn revision: 12964].
- <rlink to="html/documentation.html#ldR2c">Documentation (R2c)</rlink>.
- </body>
- <body>
- The scripts are grouped in directories, first by part, then by component.
- </body>
- <body>
- <notice class="alpha" text="Notice:"/>
- the scripts are checked by the latest version of Matita from
- <link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
- at path <trunk/matita/>.
- </body>
- </topitem>
-
<body>
Informational pages on the parts of the specification:
<rlink to="html/ground_2.html">Background</rlink>,
<rlink to="html/apps_2.html">Applications</rlink>.
</body>
+ <body>
+ <notice class="alpha" text="Notice:"/>
+ The scripts are grouped in directories, first by part, then by component.
+ </body>
+
+ <body>
+ <notice class="alpha" text="Notice:"/>
+ the scripts are checked by the latest version of Matita from
+ <link to="http://matita.cs.unibo.it/gitweb/">helm.git repository</link>.
+ </body>
+
+ <topitem name="source2B">
+ <body>
+ <rlink to="download/lambdadelta_2B.tar.bz2">lambdadelta_2B for Matita 0.99.4</rlink>
+ (revised <notice class="delta" text="2019-11"/>).
+ Source scripts [Git revision: 2019-11-19 20:45:15].
+ <rlink to="html/documentation.html#ldV2b">Documentation (V2b)</rlink>.
+ </body>
+ </topitem>
+
+ <topitem name="source2A">
+ <body>
+ <rlink to="download/lambdadelta_2A.tar.bz2">lambdadelta_2A for Matita 0.99.2</rlink>
+ (revised <notice class="delta" text="2019-11"/>).
+ Source scripts [Git revision: 2014-10-28 17:46:26].
+ <rlink to="html/documentation.html#ldR2c">Documentation (R2c)</rlink>.
+ <list><item>
+ <notice class="delta" text="2019 November 20."/>
+ repackaging (was lambdadelta_2A1).
+ </item></list>
+ </body>
+ </topitem>
+
<!-- VERSION 1 =========================================================== -->
<subsection name="v1"><img logo="ld1"/>λδ version 1 (superseded)</subsection>
<body>
The formal specification of λδ version 1
- is available in the following formats:
+ is available in the following formats.
</body>
- <topitem name="source1">
+ <body>
+ Informational pages on the parts of the specification:
+ <rlink to="html/ground_1.html">Background</rlink>,
+ <rlink to="html/basic_1.html">Core</rlink>.
+ </body>
+
+ <body>
+ <notice class="alpha" text="Notice:"/>
+ The scripts are grouped in directories, one for each part.
+ </body>
+
+ <topitem name="source1A">
<body>
- <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
- (revised <notice class="delta" text="2015-09"/>).
+ <rlink to="download/lambdadelta_1A.tar.bz2">lambdadelta_1A for Coq 7.3.1</rlink>
+ (revised <notice class="delta" text="2019-11"/>).
Source scripts.
<rlink to="html/documentation.html#ldJ1a">Documentation (J1a)</rlink>.
<list><item>
+ <notice class="delta" text="2019 November 20."/>
+ repackaging (was lambdadelta_1).
+ </item><item>
<notice class="delta" text="2015 January 15."/>
17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
</item></list>
</body>
- <body>
- The scripts are grouped in directories, one for each part.
- </body>
</topitem>
- <topitem name="static1">
- <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
- (revised <notice class="delta" text="2011-09"/>).
+ <topitem name="static1A">
+ <rlink to="static/matita/lambdadelta/">lambdadelta_1A for Matita 0.5</rlink>
+ (revised <notice class="delta" text="2019-11"/>).
Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.
<list><item>
<rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
</item></list>
</topitem>
- <topitem name="dynamic1">
+ <topitem name="dynamic1A">
<link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">
- lambdadelta_1 for Matita 0.5</link>
- (revised <notice class="delta" text="2011-09"/>).
+ lambdadelta_1A for Matita 0.5</link>
+ (revised <notice class="delta" text="2019-11"/>).
<link to="http://helm.cs.unibo.it/">HELM</link> directory.
<notice class="alpha" text="Notice: the HELM rendering engine is offline."/>
</topitem>
- <body>
- Informational pages on the parts of the specification:
- <rlink to="html/ground_1.html">Background</rlink>,
- <rlink to="html/basic_1.html">Core</rlink>.
- </body>
-
<footer/>
</page>
contrib:
@echo " TAR -cjf $(CONTRIB).tar.bz2 root $(XPACKAGES)"
- $(H)tar -cjf $(CONTRIB).tar.bz2 root $(XMAS)
+ $(H)tar -cjf $(CONTRIB).tar.bz2 ../lambdadelta/root $(XMAS:%=../lambdadelta/%)
# clean ######################################################################
</news>
<subsection name="A">Stage "A" </subsection>
+ <news class="delta" date="2019 November 20.">
+ λδ-2A is repackaged (was λδ-2A1).
+ </news>
<news class="delta" date="2015 August 27.">
λδ-2A appears too complex and is dismissed.
</news>
projects / helm.git / commitdiff