\lambda\delta home page

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fhome.html;h=59aae3134ae2de8088c6c4b08d64437624461ba8;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=c58614f4c48b42029132eba1c59e08a51ac0aeef;hpb=e866d78af74246133f5a14cb711a62af39308dee;p=helm.git diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index c58614f4c..59aae3134 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -1,99 +1,302 @@ -\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)

Foreword $\lambda\delta butterfly$

+ + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

+

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+

+ $\lambda\delta rainbow rule$ +

+

+
+

+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ home +	+ news +	+ specification +	+ +	+ +	+ documentation +	+ implementation +	+ +
+ foreword +	+ milestones +	+ version 2 +	(background - core - applications)	+ +	+ version 2 +	+ helena +	+ Open Symbolic Notation (OSN) +
+ citations +	+ visibility +	+ version 1 +	(background - core)	(static HELM directory)	+ version 1 +	+ library +	(static LDDL directory)

+

+

Foreword $\lambda\delta butterfly$ +

+

The formal systems of the Î»Î´ (\lambda\delta) family are typed Î»-calculi aiming to support the foundational frameworks for Mathematics that require an underlying specification language (for example the Minimalist Foundation and its predecessors). -

+

+

The Î»Î´ family is developed within the Hypertextual Electronic Library of Mathematics as a set of machine-checked digital specifications. -

+

+

This is the family logo: crux_177.png (revised 2012-09). -

Notice for the user of Internet Explorer. +

+

+ Notice for the user of Internet Explorer. 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. -

Citations $\lambda\delta butterfly$

+

+ +

Citations $\lambda\delta butterfly$ +

+

This is a list of publications citing Î»Î´ documentation. -

+

+

+ Matthias Weber: + An extended type system with lambda-typed lambda-expressions (extended version) + (2017). Technical report. Faculty of Computer Science, Technical University of Berlin. +

+

M.E. Maietti, S. Maschio: An extensional Kleene realizability semantics for the Minimalist Foundation (2015). In Leibniz International Proceedings in Informatics, 39, pp 162-186. Schloss Dagstuhl, Leibniz-Zentrum fÃ¼r Informatik. -

+

+

C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi: 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: 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: 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. -

Disclaimer $\lambda\delta butterfly$

+ + + +

Disclaimer $\lambda\delta butterfly$ +

+

The systems of the Î»Î´ family are not 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 (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 (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 (1994). In Lecture Notes in Computer Science, 789, pp. 516â542. Springer. -

Î»â of +

+

+ Î»â of S. Ronchi Della Rocca, L. Paolini: 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 (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 (1978). TH-report 78-WSK-03. Eindhoven University of Technology, Eindhoven. -

[Smiling face]

+ + +

+

[Smiling face]

Moreover, the systems of the Î»Î´ family are not related intentionally to Lady Lambdadelta, the Witch of Certainty of the sound novel Umineko no Naku Koro ni. -

$\lambda\delta rainbow rule$

[Valid XHTML 1.1]

[Valid CSS level 2]

[Generated from XML via XSL]

[PNG used here]

[Viewable with any browser]

Last update: Thu, 09 Mar 2017 13:38:16 +0100

+

+

+ $\lambda\delta rainbow rule$ +

+

+
+

+

[Valid XHTML 1.1]

[Valid CSS level 2]

[Generated from XML via XSL]

[PNG used here]

[Viewable with any browser]

+

+
+

+

Last update: Fri, 24 Nov 2017 21:00:00 +0100

+ +