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.