[comp.ai.digest] Conference - CMU meeting on metadeduction

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