[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