The informal proceedings of the 2nd Workshop on Logical Frameworks (Edinburgh May 1991) are now available by ftp. To obtain the document by ftp use the internet address 129.215.160.150 You should be connected to the machine 'cumbrae' at Edinburgh. Use the login name 'anonymous' (any password accepted), and the file name /export/bra/proc91.dvi.Z (file is compressed). The contents include: F. Barbanera, S.Berardi Witness Extraction in Classical Logic through Normalization D. A. Basin, R. L. Constable Metalogical Frameworks Y. Bertot A Canonical Calculus of Residuals T. Coquand A semantics of evidence for classical arithmetic R. Diaconescu, J. Goguen Logical Support for Modularisation P. Stefaneas G. Dowek A Complete Proof Synthesis Method for the Cube of Type Systems A. Felty A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs G. Huet A case study in Axiomatisation and Proof Development in the Coq Proof Assistant C. Jones Completing the Rationals and Metric Spaces in LEGO Y. Lafont Negation versus Implication S. Matthews, A. Smaill Experience with FS as a Framework D. Basin Theory T. F. Melham A Mechanized Theory of the pi-calculus in HOL D. Miller Unification of Simply Typed Lambda-Terms as Logic Programming C. Murthy Finding the Answers in Classical Proofs: A Unifying Framework T. Nipkow Order-Sorted Polymorphism in Isabelle C. Phillips Well-founded Induction and Program Synthesis Using Proof Plans D. Pym Towards an Algebraic Framework for Defining Sequential Logics J. M. Smith An Interpretation of Kleene's Slash in Type Theory N. Szasz A Machine Checked Proof that Ackermann's Function is not Primitive Recursive Claire Jones ccmj@dcs.ed.ac.uk =====================================