From: Ferruccio Guidi Date: Thu, 8 Sep 2011 20:36:58 +0000 (+0000) Subject: initial commit of lambda_delta web site X-Git-Tag: make_still_working~2297 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fba2975ffd09ffb30a60500725c9991421445f37;p=helm.git initial commit of lambda_delta web site (it was not maintained in svn so far) --- diff --git a/helm/www/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html new file mode 100644 index 000000000..e7f836acc --- /dev/null +++ b/helm/www/lambda_delta/documentation.html @@ -0,0 +1,353 @@ + + + + + lambda-delta home page + + + + + +
+
+[Crux Logo] +

The Formal System λδ (lambda-delta)
+

+

Towards the unification of terms, types, environments and contexts

+[Separator]
+ + + + + + + +
+ + +
    +
  • Papers
    • +
+ + 		+

Documentation [Butterfly]

+Currently the main source of +information on λδ (version 1) is Resource +1.1 below.
+A summary of basic λδ (version +1) is found in Resource 1.5 +below.
+

[Basic lambda-delta Logo] Basic λδ version 2:

+ + + + + + + + + + + + + + + + + + + +
2.1.
+ 		F. Guidi: An +Efficient +Validation Procedure for the Formal System λδ +(2010-07). In CiE 2010 Local Proceedings. +University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry.
+
+
2.2.
+ 		F. +Guidi: + + + + + + + + + Landau's +"Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of +Bologna, technical report UBLCS-2009-16. BibTeX entry.
+
+
2.3.
+ 		F. Guidi: An +Efficient +Validation Procedure for the Formal System λδ (2010-07). Presentation +at +CiE +2010 +(slides).
+
+
2.4.
+ 		F. Guidi: A +Validator +for the Formal System λδ (revised 2010-02). Presentation +at +the +University +of +Bologna +(slides).
+

[Basic lambda-delta Logo] Basic λδ version 1:

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
1.1.
+ 		F. +Guidi: The Formal System λδ (2009-10). In ACM ToCL 11(1), Article +No. 5 (accepted + 2008-07). CoRR +identifier cs/0611040 [v10] (revised 2008-09). BibTeX +entry.
+
+
1.2.
+ 		F. Guidi: Lambda Types on the Lambda Calculus with +Abbreviations (2007-06). +In + + + + + + + + + + + + + CiE 2007 Local Proceedings. +University +of +Siena, +technical +report +487, +p. +387 +(abstract +of +a +presentation). + + + + + + + BibTeX +entry.
+
+
1.3.
+ 		F. Guidi: Lambda Types on the Lambda Calculus with +Abbreviations (2006-11). +University +of +Bologna, +technical +report +UBLCS-2006-25. + + + + + + + + + + + + + + BibTeX +entry.
+
+
1.4.
+ 		F. Guidi: Lambda +Types +on +the +Lambda +Calculus +with +Abbreviations: +a +Certified +Specification (2006-01). +University of +Bologna, technical report UBLCS-2006-01. BibTeX entry.
+
+
1.5.
+ 		F. Guidi: The +Formal +System lambda-delta +(2008-10). Presentation at +"Advances in Constructive Topology and Logical Foundations" (slides).
+
+
1.6.
+ 		F. Guidi: Towards the Unification of Terms, Types +and Contexts (2008-03). +Presentation +at +Types +2008 +(slides).
+
+
1.7.
+ 		F. Guidi: Lambda Types on the Lambda Calculus with +Abbreviations (2007-06). +Presentation +at +CiE +2007 +(slides).
+
+
1.8.
+ 		F. Guidi: Lambda Tipi sul Lambda Calcolo con +Abbreviazioni (2007-01). +Presentation +at +the +University +of +Padova +(slides + + + + + + + in +Italian).
+
+
1.9.
+ 		F. +Guidi: Lambda Tipi sul Lambda Calcolo con +Abbreviazioni: una Specifica Certificata (2005-12). Presentation at +the University of Bologna (slides in +Italian).
+
+
+
+[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+
+Last update 2010-12-14 by Ferruccio +Guidi
+
+ + diff --git a/helm/www/lambda_delta/download/automath.sl b/helm/www/lambda_delta/download/automath.sl new file mode 100644 index 000000000..d28950a36 --- /dev/null +++ b/helm/www/lambda_delta/download/automath.sl @@ -0,0 +1,27 @@ +$1 = "Automath"; + +create_syntax_table ($1); + +define_syntax ("{","}",'%', $1); % comments +define_syntax ("#","",'%', $1); % comments +define_syntax ("%","",'%', $1); % comments +define_syntax ("([<", ")]>", '(', $1); % brackets +define_syntax ('"', '"', $1); % strings +define_syntax ("a-zA-Z_0-9`'", 'w', $1); % words +define_syntax (":+-=*@~,;.?", '+', $1); % operators + + +() = define_keywords_n ($1, "EBPN_E", 2, 0); +() = define_keywords_n ($1, "'_E''eb''pn'PRIMPROPTYPE", 4, 0); +() = define_keywords_n ($1, "'prim''prop''type'", 6, 0); + +define Automath_mode () +{ + variable kmap = "Automath"; + + set_mode(kmap, 0x04); + use_syntax_table (kmap); + runhooks("Automath_mode_hook"); +} + +add_mode_for_extension ("Automath", "aut"); diff --git a/helm/www/lambda_delta/download/b3.png b/helm/www/lambda_delta/download/b3.png new file mode 100644 index 000000000..3ed538923 Binary files /dev/null and b/helm/www/lambda_delta/download/b3.png differ diff --git a/helm/www/lambda_delta/download/b4.png b/helm/www/lambda_delta/download/b4.png new file mode 100644 index 000000000..ccfd1a99a Binary files /dev/null and b/helm/www/lambda_delta/download/b4.png differ diff --git a/helm/www/lambda_delta/download/b5.png b/helm/www/lambda_delta/download/b5.png new file mode 100644 index 000000000..30cace1d1 Binary files /dev/null and b/helm/www/lambda_delta/download/b5.png differ diff --git a/helm/www/lambda_delta/download/b9.png b/helm/www/lambda_delta/download/b9.png new file mode 100644 index 000000000..0de559867 Binary files /dev/null and b/helm/www/lambda_delta/download/b9.png differ diff --git a/helm/www/lambda_delta/download/basic_32.png b/helm/www/lambda_delta/download/basic_32.png new file mode 100644 index 000000000..350f6bcb0 Binary files /dev/null and b/helm/www/lambda_delta/download/basic_32.png differ diff --git a/helm/www/lambda_delta/download/bld.pdf b/helm/www/lambda_delta/download/bld.pdf new file mode 100644 index 000000000..469d299ac Binary files /dev/null and b/helm/www/lambda_delta/download/bld.pdf differ diff --git a/helm/www/lambda_delta/download/cie_2010.pdf b/helm/www/lambda_delta/download/cie_2010.pdf new file mode 100644 index 000000000..8afbebb26 Binary files /dev/null and b/helm/www/lambda_delta/download/cie_2010.pdf differ diff --git a/helm/www/lambda_delta/download/crux_16.ico b/helm/www/lambda_delta/download/crux_16.ico new file mode 100644 index 000000000..7323c8af8 Binary files /dev/null and b/helm/www/lambda_delta/download/crux_16.ico differ diff --git a/helm/www/lambda_delta/download/crux_32.png b/helm/www/lambda_delta/download/crux_32.png new file mode 100644 index 000000000..be5524e5e Binary files /dev/null and b/helm/www/lambda_delta/download/crux_32.png differ diff --git a/helm/www/lambda_delta/download/helena.sl b/helm/www/lambda_delta/download/helena.sl new file mode 100644 index 000000000..fc8b1903e --- /dev/null +++ b/helm/www/lambda_delta/download/helena.sl @@ -0,0 +1,28 @@ +$1 = "Helena"; + +create_syntax_table ($1); + +define_syntax ("\\*","*\\",'%', $1); % comments +define_syntax ("([{<", ")]}>", '(', $1); % brackets +define_syntax ('"', '"', $1); % strings +define_syntax ("\\a-zA-Z_0-9", 'w', $1); % words + +set_syntax_flags ($1, 4); + +() = define_keywords_n ($1, "\\ax\\th", 3, 0); +() = define_keywords_n ($1, "\\def", 4, 0); +() = define_keywords_n ($1, "\\cong\\decl\\open", 5, 0); +() = define_keywords_n ($1, "\\close\\graph\\sorts", 6, 0); +() = define_keywords_n ($1, "\\require", 8, 0); +() = define_keywords_n ($1, "\\generate", 9, 0); + +define helena_mode () +{ + variable kmap = "Helena"; + + set_mode(kmap, 0x04); + use_syntax_table (kmap); + runhooks("helena_mode_hook"); +} + +add_mode_for_extension ("helena", "hln"); diff --git a/helm/www/lambda_delta/download/helena_0.8.0.tar.gz b/helm/www/lambda_delta/download/helena_0.8.0.tar.gz new file mode 100644 index 000000000..ef78bc46b Binary files /dev/null and b/helm/www/lambda_delta/download/helena_0.8.0.tar.gz differ diff --git a/helm/www/lambda_delta/download/helena_0.8.1.tar.gz b/helm/www/lambda_delta/download/helena_0.8.1.tar.gz new file mode 100644 index 000000000..c02f7bc14 Binary files /dev/null and b/helm/www/lambda_delta/download/helena_0.8.1.tar.gz differ diff --git a/helm/www/lambda_delta/download/helena_32.png b/helm/www/lambda_delta/download/helena_32.png new file mode 100644 index 000000000..4a065aefe Binary files /dev/null and b/helm/www/lambda_delta/download/helena_32.png differ diff --git a/helm/www/lambda_delta/download/helena_label.png b/helm/www/lambda_delta/download/helena_label.png new file mode 100644 index 000000000..55487ab99 Binary files /dev/null and b/helm/www/lambda_delta/download/helena_label.png differ diff --git a/helm/www/lambda_delta/download/lambda_delta.bib b/helm/www/lambda_delta/download/lambda_delta.bib new file mode 100644 index 000000000..26c994a96 --- /dev/null +++ b/helm/www/lambda_delta/download/lambda_delta.bib @@ -0,0 +1,78 @@ +@incollection{lambdadelta7, + author="F. {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", + publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores", + address="Ponta Delgada, Portugal", + editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", + booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", + pages="204-213", + year="2010", + month="July" +} + +@techreport{lambdadelta6, + author="F. {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2009-16", + year="2009", + month="September" +} + +@article{lambdadelta5, + author="F. {Guidi}", + title="{The Formal System $\lambda\delta$}", + publisher="ACM", + address="New York, NY, USA", + journal="Transactions on Computational Logic", + volume="11", + number="1", + year="2009", + month="October", + pages="Article No. 5" +} + +@incollection{lambdadelta4, + author="F. {Guidi}", + title="{Lambda Types on the Lambda Calculus with Abbreviations}", + publisher="Universit\`a di Siena", + address="Siena, Italy", + editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", + booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", + pages="387-387", + year="2007", + month="June" +} + +@techreport{lambdadelta3, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-25", + year="2006", + month="November" +} + +@techreport{lambdadelta2, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-01", + year="2006", + month="January" +} + +@misc{lambdadelta1, + author="F. {Guidi}", + title="{lambda-delta}", + howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1", + year="2007", + month="January", + note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}" +} diff --git a/helm/www/lambda_delta/download/lambda_delta.txt b/helm/www/lambda_delta/download/lambda_delta.txt new file mode 100644 index 000000000..26c994a96 --- /dev/null +++ b/helm/www/lambda_delta/download/lambda_delta.txt @@ -0,0 +1,78 @@ +@incollection{lambdadelta7, + author="F. {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", + publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores", + address="Ponta Delgada, Portugal", + editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", + booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", + pages="204-213", + year="2010", + month="July" +} + +@techreport{lambdadelta6, + author="F. {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2009-16", + year="2009", + month="September" +} + +@article{lambdadelta5, + author="F. {Guidi}", + title="{The Formal System $\lambda\delta$}", + publisher="ACM", + address="New York, NY, USA", + journal="Transactions on Computational Logic", + volume="11", + number="1", + year="2009", + month="October", + pages="Article No. 5" +} + +@incollection{lambdadelta4, + author="F. {Guidi}", + title="{Lambda Types on the Lambda Calculus with Abbreviations}", + publisher="Universit\`a di Siena", + address="Siena, Italy", + editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", + booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", + pages="387-387", + year="2007", + month="June" +} + +@techreport{lambdadelta3, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-25", + year="2006", + month="November" +} + +@techreport{lambdadelta2, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-01", + year="2006", + month="January" +} + +@misc{lambdadelta1, + author="F. {Guidi}", + title="{lambda-delta}", + howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1", + year="2007", + month="January", + note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}" +} diff --git a/helm/www/lambda_delta/download/ld_talk_5s.pdf b/helm/www/lambda_delta/download/ld_talk_5s.pdf new file mode 100644 index 000000000..b7051c919 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_5s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_6s.pdf b/helm/www/lambda_delta/download/ld_talk_6s.pdf new file mode 100644 index 000000000..04fcec20f Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_6s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_7s.pdf b/helm/www/lambda_delta/download/ld_talk_7s.pdf new file mode 100644 index 000000000..754547c91 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_7s.pdf differ diff --git a/helm/www/lambda_delta/download/lddl.tar.bz2 b/helm/www/lambda_delta/download/lddl.tar.bz2 new file mode 100644 index 000000000..853e7a907 Binary files /dev/null and b/helm/www/lambda_delta/download/lddl.tar.bz2 differ diff --git a/helm/www/lambda_delta/download/rainbow.png b/helm/www/lambda_delta/download/rainbow.png new file mode 100644 index 000000000..45925baa7 Binary files /dev/null and b/helm/www/lambda_delta/download/rainbow.png differ diff --git a/helm/www/lambda_delta/download/xml_xsl2.png b/helm/www/lambda_delta/download/xml_xsl2.png new file mode 100644 index 000000000..00d82967b Binary files /dev/null and b/helm/www/lambda_delta/download/xml_xsl2.png differ diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html new file mode 100644 index 000000000..c046df27d --- /dev/null +++ b/helm/www/lambda_delta/implementation.html @@ -0,0 +1,274 @@ + + + + + lambda-delta home page + + + + + +
+
+[Crux Logo] +

The Formal System λδ (lambda-delta)
+

+

Towards the unification of terms, types, environments and contexts

+[Separator]
+ + + + + + + +
+ + + +
    +
  • Resources
    +
    • +
+ 		+

Computer-checked formal +specifications [Butterfly]

+ Resource +1 below provides for the statically generated natural language representation of +λδ meta-theory (faster rendering w.r.t. resource 2 below).
+ Resource 2 below provides +for the dynamically generated natural +language representation of +λδ meta-theory (powered by the HELM +rendering engine).
+Remarkably λδ was born and developed in the digital format of resource 3 below, which is not the +formal counterpart of some informal material previously written on +paper (as it happens for most currently digitalized Mathematics).
+
    +
  1. F. Guidi: LAMBDA-TYPES +(revised 2008-06). Formal +specification with the proof assistant Matita 0.5 (HTML pages generated +by the HELM +rendering engine)
    +Here are the most relevant theorems proved in the formal specification: + +
    2. +
  2. F. Guidi: LAMBDA-TYPES +(revised 2008-06). Formal +specification with the proof assistant Matita 0.5 (HELM directory).
    +
    +
    3. +
  3. F. Guidi: LAMBDA-TYPES (revised 2008-03). +Formal specification with the proof assistant Coq 7.3.1 (source +proof scripts). BibTeX entry.
    +
    4. +
+

Tools [Butterfly]

+ [Crux Logo] The λδ +Digital +Library +(LDDL) is part of HELM +and contains a set of +resources expressed in λδ.
+
    +
  • Contents: Landau's "Grundlagen der Analysis" (from +Jutting's specification in Automath).
    +
    • +
+ + +
+ [Helena Logo] Helena is a λδ +processor, +implemented in Caml as a part of +the HELM software, meant for +testing the stable features of the calculus as well as the unstable +ones.
+The processor source code is available in the directory /trunk/helm/software/lambda-delta/ +of the HELM Svn +repository. The Svn revisions containing the stable versions +of  Helena are indicated below.
+
    +
  • Version 0.8.1 (2010-11). +Exploits a subset of "complete_rg" λδ as the intermediate language. +Features importation from ".hln" files containing λδ textual syntax. +The overall validation speed of the "Grundlagen +der +Analysis" increases of 22% with respect to version 0.8.0. [Svn +revision: 11032] (archived +source code) + +
    • +
+
    +
  • Version 0.8.0 (2009-09). Supports +"basic_rg" λδ with naive implementation of impredicative sort +inclusion. Features +importation from Automath +and exportation to XML. [Svn +revision: 10304] (archived +source code)
    +
      +
    • 2009-09. +Jutting's specification of Landau's "Grundlagen +der +Analysis" enters λδ Digital Library.
      +
      • +
    • 2009-06. +Jutting's specification of Landau's "Grundlagen +der +Analysis" is +successfully processed, enabling sort inclusion.
      • +
    +
    • +
+

Other resources [Butterfly]

+ +
    +
  • A Jed mode for +editing ".hln" files (containing λδ textual syntax): helena.sl +(revised 2010-11).
    • +
+ +
    +
  • A logo for "basic" λδ: bld.pdf (revised 2008-07).
    +
    • +
+
+
+[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+
+Last update 2010-12-14 by Ferruccio +Guidi
+
+ + diff --git a/helm/www/lambda_delta/index.html b/helm/www/lambda_delta/index.html new file mode 100644 index 000000000..abc24b14e --- /dev/null +++ b/helm/www/lambda_delta/index.html @@ -0,0 +1,111 @@ + + + + + lambda-delta home page + + + + + +
+
+[Crux Logo] +

The Formal System λδ (lambda-delta)
+

+

Towards the unification of terms, types, environments and contexts

+[Separator]
+ + + + + + + +
+
    +
  • Foreword
    • +
+ + + + 		+

Foreword [Butterfly]

+The formal system λδ +(lambda-delta) is a typed lambda calculus that pursues the static and +dynamic unification of terms, types, environments and contexts while +enjoying a well-conceived meta-theory, which includes the commonly +desired properties.
+
+λδ takes some features from the calculi of the Automath family and +some from the pure type systems, but it differs from both in that it +does not include the Π construction while it provides for an +abbreviation mechanism at the level of terms.
+
+λδ features explicit type annotations, which are borrowed from +realistic type checker implementations and with which type checking is +reduced to type inference.
+
+The reduction steps of λδ include β-contraction, δ-expansion, +ζ-contraction and θ-swap. On the other hand, +η-contraction is not included.
+
+The meta-theory of λδ includes important properties such as the +confluence of reduction, the correctness of types, the +uniqueness of types up to conversion, the subject reduction of the type +assignment, the strong normalization of the typed terms. The +decidability of type inference and of type checking come as corollaries.
+
+λδ features uniformly dependent types and a predicative abstraction +mechanism, so the calculus can serve as a formal specification language +for the type theories that need a predicative foundation. λδ is +expected to have the expressive power of λ→.
+

Notice +for +the +Internet +Explorer +user [Butterfly]

+To view this site +correctly, please select a font with Unicode +support.
+For example Lucida Sans Unicode +(it should be already installed on your system).
+To change the current font follow:
+ "Tools" menu → "Internet +Options" entry → "General" tab → "Fonts" button.
+
+
+[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+
+Last update 2010-12-14 by Ferruccio +Guidi
+
+ + diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html new file mode 100644 index 000000000..fc6d4d244 --- /dev/null +++ b/helm/www/lambda_delta/news.html @@ -0,0 +1,234 @@ + + + + + lambda-delta home page + + + + + +
+
+[Crux Logo] +

The Formal System λδ (lambda-delta)
+

+

Towards the unification of terms, types, environments and contexts

+[Separator]
+ + + + + + + +
+ +
    +
  • News
    • +
+ + + 		+

News [Butterfly]

+ +
    +
  • November 2010. Helena 0.8.1 is released.
    +
    • +
+ + + +
    +
  • September 2008. +This site is online.
    +
    • +
+ + + + +
    +
  • March 2008. An +improvement of the +specification of λδ in Coq 7.3.1 begins: +
      +
    • native type assignment with new rules for application: nty (it replaces ty3);
      +
      • +
    • parallel conversion on focalized terms: fpcs (it replaces pc3); + + + + + + + +
      +
      • +
    • new weak parallel reduction on environments: wcpr (it is based on fpr and replaces wcpr0); 
      +
      • +
    • parallel reduction on focalized terms: fpr and fprs (they replace pr2, pr3);
      +
      • +
    +
      +
    • new thinning relation: drop +(it replaces the old drop, clear, getl, cimp, drop1);
      • +
    • new shift function: shift: +(it +replaces + app1);
      • +
    • new length function for environments: clen;
      +
      • +
    • new relocation function: lift (it replaces old lift, lift1);
      +
      • +
    • new term structure with polarity indicators and no +distinction between binding and flat items;
      • +
    • new general theory of relocation (comprises new +relocation functions: s, r);
      • +
    • we removed context-free reduction and conversion (pr0, pr1, pc1);
      +
      • +
    • we removed greedy substitution (csubst0, + + + csubst1, fsubst0, subst0, subst1);
      +
      • +
    • we removed level indicators on environments (cbk).
      • +
    +
    • +
+ + + +

Visibility [Butterfly]

+
    +
  • November 2010. The Google +search formal system lambda delta +gives 8 resources about λδ as the first results.
    +
    • +
+
    +
  • November 2010. The Yahoo +search formal system lambda delta +gives 4 resources and 2 sub-resources about λδ as the first results.
    • +
+
+
+[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+
+Last update 2010-12-14 by Ferruccio +Guidi
+
+ +