web site update

[helm.git] / helm / coq-contribs / lambdadelta / web / basic_1.ldw.xml
diff --git a/helm/coq-contribs/lambdadelta/web/basic_1.ldw.xml b/helm/coq-contribs/lambdadelta/web/basic_1.ldw.xml

new file mode 100644 (file)

index 0000000..d54d03e
--- /dev/null
+++ b/helm/coq-contribs/lambdadelta/web/basic_1.ldw.xml
@@ -0,0 +1,49 @@
+<?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>