Registro:

Referencias:

• Berardi, S., Towards a mathematical analysis of the Coquand-Huet calculus of construction and the other systems in Barendregt's cube (1988), Technical Report, Department of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino; Terlouw, J., (1989) Een Nadere Bewijstheoretische Analyse van GSTT's, , Technical Report, Department of Computer Science, University of Nijmegen
• Barendregt, H.P., Lambda calculi with types (1992) Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures, pp. 117-309. , In Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds); Oxford University Press, Oxford
• Church, A., A formulation of the simple theory of types (1940) J. Symbolic Logic, 5, pp. 56-68
• Coquand, T., Une théorie des constructions (1985), PhD Thesis, Université Paris VII, Thèse de troisième cycle; Coquand, T., Huet, G., The calculus of constructions (1988) Inform. Comput., 76, pp. 95-120
• Hindley, J.R., Seldin, J.P., (1986) Introduction to Combinators and λ-Calculus (London Mathematical Society Student Texts, Vol. 1), , Cambridge University Press, Cambridge, UK
• De Bruijn, N.G., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation with application to the Church Rosser theorem (1972) Selected Papers on Automath (Studies in Logic and the Foundations of Mathematics, Vol. 133), , In Nederpelt, R. P., Geuvers, J.H. and de Vrijer, R. C. (eds); North-Holland, Amsterdam
• Pfenning, F., (1992) A Proof of the Church Rosser Theorem and Its Representation in a Logical Framework, , Technical Report CMU-CS-92-186, Carnegie Mellon University
• McKinna, J., Pollack, R., Pure type systems formalised (1993) Proc. Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93, 664, pp. 289-305. , In Bezem, M. and Groote J.-F. (eds); Lecture Notes in Computer Science; Springer-Verlag, Utrecht
• Rose, K.H., Operational reduction models for functional programming languages (1996), PhD Thesis, University of Copenhagen; Kamareddine, F., Ríos, A., Bridging de Bruijn indices and variable names in explicit substitutions calculi (1998) Logic J. Interest Group Pure Appl. Logic, IGPL, 6, pp. 843-874
• Barendregt, H.P., (1984) The Lambda Calculus: Its Syntax and Semantics. (Studies in Logic and the Foundations of Mathematics, Vol. 103) (Revised Edition), , North-Holland, Amsterdam
• (1994) Selected Papers on Automath (Studies in Logic and the Foundations of Mathematics, Vol. 133), , Nederpelt, R. P., Geuvers, J. H. and de Vrijer, R. C. (eds); North-Holland, Amsterdam
• Harper, R., Honsell, F., Plotkin, G., A framework for defining logics (1987) Proc. Second Symposium on Logic in Computer Science, pp. 194-204. , IEEE, Washington DC
• Milner, R., Tofte, M., Harper, R., (1990) Definition of Standard ML, , MIT Press, Cambridge, MA
• Kamareddine, F., Ríos, A., A λ-calculus à la de Bruijn with explicit substitutions (1995) Proc. 7th Int. Symp. on Programming Languages: Implementations, Logics and Programs, PLILP'95, Lecture Notes in Computer Science, 982, pp. 45-62. , Springer-Verlag, Utrecht
• Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit substitutions (1991) J. Functional Programming, 1, pp. 375-416
• Kamareddine, F., Ríos, A., Wells, J.B., Calculi of generalised β-reduction and explicit substitution: Type free and simply typed versions (1998) J. Functional Logic Programm., pp. 1-44
• Kamareddine, F., Bloo, R., Nederpelt, R.P., On π-conversion in the λ-cube and the combination with abbreviations (1999) Ann. Pure Appl. Logics, 97, pp. 27-45

Citas:

---------- APA ----------

---------- CHICAGO ----------

---------- MLA ----------

---------- VANCOUVER ----------