arvind@utcsri.UUCP (11/18/87)
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