[Next][Index][Thread]

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
      TPS, WeH 7211, by Sunil Issar and Dan Nesmith