[1] H. Barendregt, The impact of the lambda calculus in Logic and Computer Science, "Bullettin of Symbolic Logic", 3, 1997, pp. 191-215.

[2] H.P. Barendregt, Lambda calculi with types, in "Handbook of Logic in Computer Science", S. Abramsky, D. Gabbay, and T.S.E. Maibaum (eds.), vol. 2, ch. 2, Oxford University Press, 1992, pp. 117-309.

[3] E. Giménez, A tutorial on recursive types in Coq, Technical report, INRIA, 1998.

[4] R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, "Journal of the Association for Computing Machinery", 40/1, 1993, pp. 143-184. [Available in DVI format].

[5] F. Honsell, M. Miculan, and I. Scagnetto, p -calculus in (co)inductive type theory, "Theoretical Computer Science", 253/2, 2001, pp. 239-285.

[6] F. Honsell, M. Miculan, and I. Scagnetto, An axiomatic approach to metareasoning on systems, in "HOAS, ICALP ’01", LNCS 2073, 2001.

[7] F. Honsell, M. Lenisa, U. Montanari, and M. Pistore, Final semantics for the p -calculus, in "Proc. PROCOMET ’98", 1998.

[8] B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, "Bull. EATCS 62", 1997.

[9] R. Milner, Function as Processes, "MSCS", 2, 1992, pp. 119-141.

[10] J. Parrow, An Introduction to the p -calculus, in "Handbook of Process Algebra", Elsevier, 2001.

[11] F. Pfenning, The practice of logical frameworks, in "Proceedings of the Colloquium on Trees in Algebra and Programming", H. Kirchner (ed.), Linköping, Sweden, April 1996, Springer-Verlag LNCS 1059, pp. 119-134. [Available in PostScript formats].