DANIEL.LEIVANT@THEORY.CS.CMU.EDU (11/16/87)
[Forwarded from TheoryNet.] Below is the schedule of a meeting that has taken place at Carnegie Mellon University, on METALANGUAGE AND TOOLS FOR MECHANIZING FORMAL DEDUCTIVE THEORIES Please address requests for abstracts of talks to jfm@k.gp.cs.cmu.edu (ARPAnet). Friday, November 13 9:00 Using a Higher-Order Logic Programming Language to Implement Program Transformations Dale Miller, University of Pennsylvania 9:45 Building Proof Systems in an Extended Logic Programming Language Amy Felty, University of Pennsylvania 10:45 The Categorical Abstract Machine, State of the Art Pierre-Louis Curien, Ecole Normale Superieure, Paris VII 1:15 A Very Brief Look at NuPRL Joseph Bates, Carnegie Mellon University 1:45 Reasoning about Programs that Construct Proofs Robert Constable, Cornell University 2:30 Theorem Proving via Partial Reflection Douglas Howe, Cornell University 3:15 MetaPrl: A Framework for Knowledge Based Media Joseph Bates, Carnegie Mellon University 4:00 Discussion: The Role of Formal Reasoning in Software Development 5:00 Demos until 6:30 NuPRL in Wean Hall 4114 by Doug Howe Lambda Prolog in WeH 4623 by Dale Miller, Gopalan Nadathur, and Amy Felty Saturday, November 14 9:00 A Framework for Defining Logics Robert Harper, Edinburgh University 9:45 The Logician's Workbench in the Ergo Support System Frank Pfenning, Carnegie Mellon University 10:45 A Tactical Approach to Algorithm Design Douglas Smith, Kestrel Institute 11:30 Reusing Data Structure Designs Allen Goldberg, Kestrel Institute 1:15 Paddle: Popart's Development Language David Wile, University of Southern California 2:00 Mechanizing Construction and Modification of Specifications Martin Feather, University of Southern California 3:00 The TPS Theorem Proving System Peter Andrews, Carnegie Mellon University 3:45 ONTIC: Knowledge Representation for Mathematics David McAllester, Cornell University 4:30 Demos until 6:00 Popart and Paddle in the KBSA, Wean Hall 4114, by David Wile and Martin Feather The LF Proof Editor, Wean Hall 4623, by Robert Harper