The SLIMMER Project

SLIMMER is a collaborative project between INRIA, France and the University of Minnesota. This project concerns applications of proof search broadly construed—SLIMMER is an acronym for "Sophisticated Logic Implementations for Modeling and MEchanical Reasoning." The current focus of the research 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 computation systems, specification and reasoning demand different support from underlying implementations. This project brings together researchers who are actively designing specification and reasoning systems as well as developing implementation of such logics.


Financial support for the project has been obtained from INRIA (for the French side) and the NSF (for the U.S. side). This funding is presently in the form of grants that support travel for the project personnel between the two sites. The support from INRIA is provided via its "Equipes Associées" program, with the recognition of SLIMMER as an Associated Teams project. The NSF support derives from the CISE Directorate and the Office of International Science and Engineering.


The current participants in this project are the members of the Parsifal and Teyjus projects. The people involved are the following:



The following papers by project personnel have a bearing on the collaborative research:


If coordinated development of this system is of interest, we can consider using cvs and/or sourceforge. A rough tranlation to ocaml of this ML code is available on request.

Related Sites and Other Relevant Systems

Future Plans

This project was initially designed to bring together the Parsifal and Teyjus teams with the objective of exploring the use of the modern day understanding of proof search in building sophisticated systems for modelling and reasoning about models. We hope to expand the present scope of this project both by diversifying its personnel pool and by expanding its resources. We invite interested potential partners and participants to contact Dale Miller or Gopalan Nadathur.