]> matita.cs.unibo.it Git - helm.git/commitdiff
new web site page
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 18 Sep 2019 16:36:13 +0000 (18:36 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 18 Sep 2019 16:36:13 +0000 (18:36 +0200)
change log for λδ begins

.gitignore
helm/www/lambdadelta/alt.sh [new file with mode: 0644]
helm/www/lambdadelta/web/home/changes.ldw.xml [new file with mode: 0644]
helm/www/lambdadelta/web/home/changes.tbl [new file with mode: 0644]

index a49af21b84b46e3fa114ff725fb780157f6500b3..e7228e3ba6538d1b96b59a22207bd2b05f9b4968 100644 (file)
@@ -66,6 +66,7 @@ helm/www/lambdadelta/xslt/documentation_3.xsl
 helm/www/lambdadelta/xslt/sitemap.xsl
 helm/www/lambdadelta/xslt/versions.xsl
 helm/www/lambdadelta/xslt/core.xsl
+helm/www/lambdadelta/xslt/changes.xsl
 helm/www/lambdadelta/xslt/chc_45.xsl
 helm/www/lambdadelta/xslt/xhtbl.xsl
 
diff --git a/helm/www/lambdadelta/alt.sh b/helm/www/lambdadelta/alt.sh
new file mode 100644 (file)
index 0000000..80a326f
--- /dev/null
@@ -0,0 +1 @@
+sed s?lambdadelta.info?www.cs.unibo.it/~fguidi/lambdadelta?g html/$1.html > html/$1.alt.html
diff --git a/helm/www/lambdadelta/web/home/changes.ldw.xml b/helm/www/lambdadelta/web/home/changes.ldw.xml
new file mode 100644 (file)
index 0000000..4287ac5
--- /dev/null
@@ -0,0 +1,17 @@
+<?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 = "The Formal Systems of the λδ (\lambda\delta) Family"
+>
+   <sitemap name="sitemap"/>
+
+   <section15 name="changes">Changes</section15>
+   <body>
+   </body>
+   <table name="changes"/>
+
+   <footer/>
+</page>
diff --git a/helm/www/lambdadelta/web/home/changes.tbl b/helm/www/lambdadelta/web/home/changes.tbl
new file mode 100644 (file)
index 0000000..d25be28
--- /dev/null
@@ -0,0 +1,118 @@
+name "changes"
+
+table {
+  class "gray"
+  [ "version" [ "aspect" [ "" "changes" ]]
+  ]
+
+  class "orange"
+  [ { "λδ-2B" + "(unreleased)" * }
+    {
+     [ [{ "equivalences" * }]
+       { "+" "+" "+" "-" }
+       { "equivalence for full rt-reduction (terms)"
+         "equivalence for whd rt-reduction (terms)"
+         "equivalence for extended rt-reduction (terms, referred lenvs, closures)"
+         "syntactic equivalence (closures) removed"
+       }
+     ]
+     [ [{ "weights" * }]
+       { "+" }
+       { "switch in primitive order relations for closures to enable the exclusion binder"
+       }
+     ]
+     [ [{ "relocation" * }]
+       { "" }
+       { ""
+       }
+     ]
+     [ [{ "syntax" * }]
+       { "+" }
+       { "exclusion binder for lenvs"
+       }
+     ]
+     [ [{ "ground" * }]
+       { "+" "*" "+" "-" }
+       { "rt-transition counters"
+         "generic reference transforming maps as streams of non-negative integers" 
+         "extensional equality, labelled transitive closures and streams"
+         "non-negative integers with infinity removed"
+       }
+     ]
+    }
+  ]
+
+  class "orange"
+  [ { "λδ-2A" + "(October 2014)" * }
+    {
+     [ [{ "equivalences" * }]
+       { "+" }
+       { "syntactic equivalence (selected lenvs, referred lenvs, closures)"
+       }
+     ]
+     [ [{ "weights" * }]
+       { "*" "-" }
+       { "primitive order relations for closures"
+         "complex weight (terms) removed"
+       }
+     ]
+     [ [{ "relocation" * }]
+       { "-" }
+       { "level update functions removed"
+       }
+     ]
+     [ [{ "syntax" * }]
+       { "+" "+" "+" "-" "-" }
+       { "polarized binders for terms"
+         "non-negative integer global references for terms"
+         "syntactic support for genvs with typed abstraction, abbreviation"
+         "numbered sorts, application, type annotation removed from lenvs"
+         "exclusion binder removed from terms and lenvs"
+       }
+     ]
+     [ [{ "ground" * }]
+       { "+" "+" }
+       { "lists and non-negative integers with infinity"
+         "library extension for transitive closures and booleans"
+       }
+     ]
+    }
+  ]
+
+  class "red"
+  [ { "λδ-1A" + "(November 2006)" * }
+    {
+     [ [{ "equivalences" * }]
+       { "" }
+       { "equivalence for outer reduction (terms)"
+       }
+     ]
+     [ [{ "weights" * }]
+       { "" "" "" }
+       { "order relations (terms, lenvs, closures) based on weights" 
+         "simple weights (terms, lenvs, closures)"
+         "complex weight (terms)"
+       }
+     ]
+     [ [{ "relocation" * }]
+       { "" }
+       { "level update functions"
+       }
+     ]
+     [ [{ "syntax" * }]
+       { "" "" }
+       { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation"
+         "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation" }
+     ]
+     [ [{ "ground" * }]
+       { "" "" }
+       { "finite reference transforming maps as compositions of basic ones"
+         "library extension for logic and non-negative integers"
+       }
+     ]
+    }
+  ]
+
+}
+
+class "center" { 2 }