Andrew Gacek and Gopalan Nadathur, University of Minnesota


Thursday, June 30 - Friday, July 1, 2005


Room 405, Walter Library (Digital Technology Center, University of Minnesota)

Motivation and Scope

This workshop is intended to bring together researchers interested in implementation aspects of proof search, especially as it relates to metalanguages and logical frameworks. In this present instance, it is loosely coupled to the SLIMMER project, a collaborative enterprise between the University of Minnesota and INRIA that is being funded by the NSF and INRIA. SLIMMER's current focus is on developing and implementing a formal framework for the specification of various kinds of computational systems and for formally reasoning about properties of these specifications. Target specification languages are those that typically involve high-levels of abstraction and symbolic computation. Recent work has illustrated that while logic can be used to both specify and reason about computational systems, specification and reasoning demand different support from underlying implementations. The purpose of this workshop is to begin a discussion between interested researchers towards understanding:

This is the first workshop in what is expected to be a series to be held at University of Minnesota, INRIA Futurs/Ecole Polytechnique or possibly colocated with conferences of mutual interest. Also, while the workshop is initiated by the SLIMMER project members, it will include "outside participants" even in its first version and is expected to set the tone for larger collaborations on the general topic of modern applications and implementations of proof search.


Times include presentation and discussion.

10:00 A.M. - 10:15 A.M. Opening Remarks
10:15 A.M. - 11:45 A.M. Explicit Substitutions through the Eyes of the Suspension Calculus

Andrew Gacek, University of Minnesota

11:45 A.M. - 2:00 P.M. Lunch Break
2:00 P.M. - 3:15 P.M. An Example of Language Translation and Proof using Higher-Order Abstract Syntax

Mike Whalen, University of Minnesota and Rockwell Collins

3:15 P.M. - 3:45 P.M. Refreshments Break
3:45 P.M. - 5:00 P.M. Contextual Modal Type Theory: A Foundation for Meta-variables

Brigitte Pientka, McGill University

9:30 A.M. - 10:30 A.M. A Logic for Reasoning about Logic Specifications

Dale Miller, INRIA-Futurs and LIX

10:30 A.M. - 11:00 A.M. Refreshments Break
11:00 A.M. - 12:00 P.M. Strategies for the Representation and Reduction of Lambda Terms and their Impact

Chuck Liang, Hofstra University

12:00 P.M. - 2:00 P.M. Lunch Break
2:00 P.M. - 3:15 P.M. Practical Higher-Order Pattern Unification with On-the-Fly Raising

Gopalan Nadathur, University of Minnesota

3:15 P.M. - 3:45 P.M. Refreshments Break
3:45 P.M. - 4:45 P.M. Treatment of Types in an Implementation of λProlog Organized around Higher-Order Pattern Unification

Xiaochu Qi, University of Minnesota

4:45 P.M. - 5:00 P.M. Wrap-Up



This incarnation of the workshop is being held under the aegis of the Digital Technology Center, University of Minnesota that has kindly consented to the use of its facilities.