Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!uunet!husc6!bloom-beacon!oberon!cit-vax!ucla-cs!zen!ucbvax!THEORY.CS.CMU.EDU!DANIEL.LEIVANT
From: DANIEL.LEIVANT@THEORY.CS.CMU.EDU
Newsgroups: comp.ai.digest
Subject: Conference - CMU meeting on metadeduction
Message-ID: <8711250813.AA18719@ucbvax.Berkeley.EDU>
Date: Mon, 16-Nov-87 10:17:49 EST
Article-I.D.: ucbvax.8711250813.AA18719
Posted: Mon Nov 16 10:17:49 1987
Date-Received: Sat, 28-Nov-87 17:52:50 EST
Sender: usenet@ucbvax.BERKELEY.EDU
Reply-To: TheoryNet List <THEORYNT%NDSUVM1.BITNET@forsythe.stanford.edu>
Organization: The ARPA Internet
Lines: 71
Approved: ailist@kl.sri.com


                     [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