Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!utgpu!utcsri!arvind
From: arvind@utcsri.UUCP
Newsgroups: ut.theory
Subject: THEORY NET: CMU meeting on metadeduction
Message-ID: <5682@utcsri.UUCP>
Date: Wed, 18-Nov-87 15:27:28 EST
Article-I.D.: utcsri.5682
Posted: Wed Nov 18 15:27:28 1987
Date-Received: Fri, 20-Nov-87 22:30:43 EST
Distribution: ut
Organization: CSRI, University of Toronto
Lines: 72

Date:         16 Nov 1987 10:17:49-EST (Monday)
From: DANIEL.LEIVANT@theory.cs.cmu.edu
Subject:      CMU meeting on metadeduction

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