<?xml version="1.0" encoding="UTF-8"?>
-<ld:page xmlns:ld="http://lambda_delta.info"
+<page xmlns="http://lambda_delta.info"
description = "lambda_delta version 2"
title = "lambda_delta version 2"
- head = "cic:/matita/lambda_delta/Basic_2/ (λδ version 2)"
+ head = "cic:/matita/lambda_delta/basic_2/ (λδ version 2)"
>
- <ld:section>Logical structure of the contribution</ld:section>
- <ld:body>The source files are grouped in planes and components according to the following table.</ld:body>
- <ld:table name="ld_basic_2_src"/>
- <ld:section>Physical structure of the contribution</ld:section>
- <ld:body>The source files are grouped in directories, one for each component.</ld:body>
- <ld:footer/>
-</ld:page>
+ <section>System's Syntax and Behavior</section>
+ <body>This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </body>
+ <table name="ld_basic_2_blk"/>
+ <body>* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </body>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="ld_basic_2_sum"/>
+ <news date="In progress.">
+ Context-sensitive subject equivalence
+ for native type assignment.
+ </news>
+ <news date="In progress.">
+ Context-sensitive subject equivalence
+ for atomic arity assignment.
+ </news>
+ <news date="2012 March 15.">
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news date="2012 January 27.">
+ Support for abstract candidates of reducibility.
+ </news>
+ <news date="2011 September 21.">
+ Confluence for context-sensitive parallel reduction.
+ </news>
+ <news date="2011 September 6.">
+ Confluence for context-free parallel reduction.
+ </news>
+ <news date="2011 April 17.">
+ Specification starts.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>The source files are grouped in planes and components
+ according to the following table.
+ A notation file covering the whole specification is provided.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses.
+ </body>
+ <table name="ld_basic_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
projects / helm.git / blobdiff