X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Findex.ldw.xml;h=5110c14703bf1f775c64e5b52b4ccc6c9361e077;hb=6b022cf2cccae67144ff045415e748b0b5c3a3d9;hp=9ebac8e8069440e00a9906da6ac5850e41aaa8e6;hpb=d966abb5707d0ce51be932b7bde99d4325d23a0c;p=helm.git diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index 9ebac8e80..5110c1470 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -21,10 +21,10 @@ This is the family logo: crux_177.png - (revised ). + (revised ). - + 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). @@ -41,43 +41,43 @@ C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi: - - (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468. + ELPI: fast, Embeddable, λProlog Interpreter + (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer. A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: - - (2012). In JAR 49(3), pp. 427-451. + Formal metatheory of programming languages in the Matita interactive theorem prover + (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer. M.E. Maietti: - + Consistency of the minimalist foundation with Church thesis and Bar Induction (2012). Submitted article. W. Ricciotti: - + Theoretical and implementation aspects in the mechanization of the metatheory of programming languages (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. C.E. Brown: - + Faithful Reproductions of the Automath Landau Formalization (2011). Technical report. M.E. Maietti: - - (2009). In APAL 160(3), pp. 319-354. + A minimalist two-level foundation for constructive mathematics + (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. V. Rahili: - + First Year Report: Realisability methods of proof and semantics with application to expansion (July 2007). Technical report. @@ -85,59 +85,59 @@ Disclaimer - The systens of the λδ family are not related intentionally to any other system + The systens of the λδ family related intentionally to any other system having (variations of) the symbols λ and δ in its name or syntax. Examples include (but are not limited to): - λ-δ of + λ-δ of A. Church: - The calculi of lambda-conversion + The calculi of lambda-conversion (1941). Annals of Mathematics Studies 6. Princeton University Press. - ∆Λ of + ∆Λ of N.G. de Bruijn: - Generalizing Automath by means of a lambda-typed lambda calculus + Generalizing Automath by means of a lambda-typed lambda calculus (1987). In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92. Marcel Dekker. - λ∆ of + λ∆ of N.J. Rehof, M.H. Sørensen: - The λ∆-calculus + The λ∆-calculus (1994). In Lecture Notes in Computer Science, 789, pp. 516–542. Springer. - λ∆ of + λ∆ of S. Ronchi Della Rocca, L. Paolini: - The Parametric Lambda Calculus + The Parametric Lambda Calculus (2004). Texts in Theoretical Computer Science, An EATCS Series. Springer. - λD of + λD of R. Nederpelt, H. Geuvers: - Type Theory and Formal Proof + Type Theory and Formal Proof (2014). Cambridge University Press. - Cλξ of + Cλξ of N.G. de Bruijn: - A namefree lambda calculus with facilities for internal definition of expressions and segments + A namefree lambda calculus with facilities for internal definition of expressions and segments (1978). TH-report 78-WSK-03. Eindhoven University of Technology, Eindhoven.