🚀 go-pugleaf

			      Workshop Program

			      PROOFS AND TYPES

			  Friday, November 13, 1992
			   in conjunction with the
      Joint International Conference and Symposium on Logic Programming,
		 November 9-13, 1992, Washington, DC, U.S.A.

Organizing Committee:
  James Harland <jah@cs.mu.oz.au>, University of Melbourne
  Frank Pfenning <fp@cs.cmu.edu>, Carnegie Mellon University
  David Pym <dpym@lfcs.ed.ac.uk>, University of Edinburgh

Session 1

8:30-9:10
Reflections on the Foundations of Meta-Programming: Is a Type Theory Needed?
Francois Bry, ECRC

9:10-9:50
Combining Prescriptive and Taxonomic Types in Logic Programming
Pat Hill, University of Leeds

9:50-10:10
Soft Sorting: Integrating Static and Dynamic Sort Checking
Jian Chen, University of Queensland

--- 30 min break

Session 2

10:40-11:20
GCLA II : A Definitional Approach to Control
Per Kreuger, SICS

11:20-12:00
Finite Term Constraints and Their Use in GCLA
Martin Aronsson, SICS

--- lunch break

Session 3

1:30-2:10
Relating Logic Programming and Propositions-as-Types: A Logical Compilation
Jim Lipton, University of Pennsylvania

2:10-2:50
Towards Proof-Theoretic Characterizations of Constraint Logic
  Programming Languages
James Andrews, Simon Fraser University

2:50-3:10
Exploiting Proofs: Implementing Meta-theory in Elf
Frank Pfenning, Carnegie Mellon University

--- 30 min break

Session 4

3:40-4:20
A Logic Programming Language Based on ECC
Dominic Duggan, University of Waterloo

4:20-4:40
Types as Theories
Mario Florido and Luis Damas, University of Porto

--- 20 min break

Session 5

5:00-5:20
A Proof-Theoretical Reconstruction of Logic Programming
Mario Ornaghi, Universita di Milano and Alberto Momigliano, CMU

5:20-5:40
Unification of Higher-Order Patterns is Linear
Zhenyu Qian, University of Bremen