[1] S. Agerhold and J. Frost, An Isabelle-based theorem prover for VDM-SL, "Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’97)", E. Gunter and A. Felty (eds.), Murray Hill, New Jersey, 1997, pp. 1-16.

[2] P. Anderson, Program extraction in a logical framework setting, in "Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning", F. Pfenning (ed.), Kiev, Ukraine, July 1994, Springer-Verlag, pp. 144-158.

[3] A.W. Appel and E.W. Felten. Proof-carrying authentication, in "Proceedings of the 6th Conference on Computer and Communications Security", G. Tsudik (ed.), Singapore, November 1999, ACM Press.

[4] A. Avron, F. Honsell, I.A. Mason, and R. Pollack, Using typed lambda calculus to implement formal systems on a machine, "Journal of Automated Reasoning", 9/3, 1992, pp. 309-354 [ A preliminary version appeared as University of Edinburgh Report ECS-LFCS-87-31] .

[6] A. Avron, F. Honsell, M. Miculan, C. Paravano, Encoding Modal Logics in Logical Frameworks, "Studia Logica", 1, 1998.

[7] 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.

[8] D.A. Basin, Logic frameworks for logic programs, in "4th International Workshop on Logic Program Synthesis and Transformation", Pisa, Italy, June 1994. Springer-Verlag LNCS 883, pp. 1-16. [Available in PostScript format].

[9] Y. Bertot, G. Kahn, and L. Théry, Proof by pointing, in "Proceedings of the International Symposium on Theoretical Aspects of Computer Softward", M. Hagiya and J.C. Mitchell (eds.), Sendai, Japan, April 1994. Springer-Verlag LNCS 789, pp. 141-160. [Available in PostScript format].

[10] R. Burstall and F. Honsell, Operational semantics in a natural deduction setting, in "Logical Frameworks", Gérard Huet and Gordon Plotkin, (eds.), Cambridge University Press, 1991, pp. 185-214.

[11] J.L. Chirimar, Proof Theoretic Approach to Specification Languages, PhD Thesis, University of Pennsylvania, 1995. [Available in PostScript format].

[12] R. Constable and D. Howe, NuPrl as a general logic, in "Logic and Computation", P. Odifreddi (ed.), Academic Press, 1990.

[13] N.G. de Bruijn, A survey of the project AUTOMATH, in "Essays in Combinatory Logic, Lambda Calculus and Formalism", in J.P. Seldin and J.R. Hindley (eds.), To H.B. Curry, Academic Press, 1980, pp. 579-606.

[14] J. Despeyroux, A. Felty, and A. Hirschowitz, Higher-order abstract syntax in Coq, in "Proceedings of the International Conference on Typed Lambda Calculi and Applications", M. Dezani-Ciancaglini and G. Plotkin (eds.), Edinburgh, Scotland, April 1995, Springer-Verlag LNCS 902, pp. 124-138. [Available in PostScript format].

[15] G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner, The Coq proof assistant user's guide, Rapport Techniques 154, INRIA, Rocquencourt, France, 1993 [ Version 5.8] .

[16] S. Feferman, Finitary inductive systems, in "Proceedings of Logic Colloquium '88", R. Ferro (ed.), pp. 191-220, Padova, Italy, August 1988, North-Holland.

[17] P. Gardner, Representing Logics in Type Theory, PhD Thesis, University of Edinburgh, 1992 [ Available as Technical Report CST-93-92] .

[18] M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.

[19] J. Hannan, Extended natural semantics, "Journal of Functional Programming", 3/2, 1993, pp. 123-152.

[20] J. Hannan and F. Pfenning, Compiler verification in LF, in "Seventh Annual IEEE Symposium on Logic in Computer Science", Andre Scedrov (ed.), Santa Cruz, California, 1992, pp. 407-418. [Available in PostScript formats].

[21] 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].

[22] D. Hirschkoff, A full formalization of pi-calculus theory in the Calculus of Constructions, in "Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97)", E. Gunter and A. Felty (eds.), Murray Hill, New Jersey, 1997, pp. 153-169.

[23] M. Hofmann, Semantical analysis for higher-order abstract syntax, in "Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS'99)", G. Longo (ed.), Trento, Italy, IEEE, Computer Society Press, 1999, pp. 204-213.

[24] F. Honsell, M. Miculan, A Natural Deduction Approach to Dynamic Logics, in "Proceedings of TYPES'95", n. 1158 in Lecture Notes in Computer Science, B. Coppo (ed.), 1996, pp.165-182.

[25] F. Honsell, M. Miculan, I. Scagnetto, Pi-calculus in (Co)Inductive Type Theories, in "Theoretical Computer Science", 253/2, 2001, pp. 239-285.

[26] Kolyang, T. Santen, and B. Wolff, A structure preserving encoding of Z in Isabelle/HOL, in "Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics", J. von Wright, J. Grundy, and J. Harrison (eds.), Turku, Finland, August 1996, Springer-Verlag LNCS 1125, pp. 283-298.

[27] Z. Luo and R. Pollack, The LEGO proof development system: A user's manual, Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992.

[28] L. Magnusson and B. Nordström, The ALF proof editor and its proof engine, in "Types for Proofs and Programs", H. Barendregt and T. Nipkow (eds.), Springer-Verlag LNCS 806, 1994, pp. 213-237.

[29] P. Martin-Löf, On the meanings of the logical constants and the justifications of the logical laws, Technical Report 2, Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Università di Siena, 1985.

[30] I.A. Mason. Hoare's logic in the LF, Technical Report ECS-LFCS-87-32, Laboratory for Foundations of Computer Science, University of Edinburgh, 1987.

[31] S. Michaylov and F. Pfenning, Natural semantics and some of its meta-theory in Elf, in "Proceedings of the Second International Workshop on Extensions of Logic Programming", L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister (eds.), Stockholm, Sweden, January 1991, Springer-Verlag LNAI 596, pp. 299-344. [Available in PostScript formats].

[32] M. Miculan, The expressive power of structural operational semantics with explicit assumptions, in "Types for Proofs and Programs", H. Barendregt and T. Nipkow (eds.), Springer-Verlag LNCS 806, 1994, pp. 263-290.

[33] M. Miculan, On the formalization of the modal mu-calculus in the Calculus of Inductive Constructions, "Information and Computation", 2001.

[34] M. Miculan, Encoding Logical Theories of Programs, PhD Thesis TD-7/97, Dipartimento di Informatica, Università di Pisa, 1997.

[35] T. Nipkow and D. von Oheimb, Java-light is type-safe – definitely, in "Conference Record of the 25th Symposium on Principles of Programming Languages (POPL'98)", in L. Cardelli (ed.), San Diego, California, ACM Press, 1998, pp. 161-170.

[36] L.C. Paulson, Isabelle: A Generic Theorem Prover, Springer-Verlag LNCS 828, 1994.

[37] L.C. Paulson, Mechanized proofs of security protocols: Needham-Schroeder with public keys, Technical Report 413, University of Cambridge, Computer Laboratory, 1997.

[38] L.C. Paulson, The inductive approach to verifying cryptographic protocols, "Journal of Computer Security", 6, 1998, pp. 85-128. [Available in PostScript format].

[39] F. Pfenning, Elf: A language for logic definition and verified meta-programming, In "Fourth Annual Symposium on Logic in Computer Science", Pacific Grove, California, IEEE Computer Society Press, 1989, pp. 313-322. [Available in PostScript formats].

[40] 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].

[41] F. Pfenning and C. Elliott, Higher-order abstract syntax, in "Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation", Atlanta, Georgia, June 1988, pp. 199-208. [Available in PostScript format].

[42] R. Pollack, How to believe a machine-checked proof, in "Twenty-Five Years of Constructive Type Theory", G. Sambin and J. Smith (eds.), Oxford University Press, August 1998, Proceedings of a Congress held in Venice, Italy, October 1995. [Available in PostScript format].

[43] L. Thery, Y. Bertot, and G. Kahn, Real theorem provers deserve real user-interfaces, in "Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments", 1992, pp. 120-129 [ Published as SIGSOFT Software Engineering Notes, vol. 17, No. 5] .