Sophisticated Logic Implementations for Modeling and Mechanical Reasoning

Contents: description / people / funding / code / publications / links /


The SLIMMER project has been focused on developing and implementing formal frameworks 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. When symbolic computations require bindings within linguistic expressions, the lambda-tree syntax approach to higher-order abstract syntax is used. The project is also focusing on the relational style of specifications that are commonly used to specify structured operational semantics and typing judgments. System building within this project have typically involved the implementation of higher-order pattern unification and of backtracking proof search engines (as is found in, for example, λProlog).

One use of the systems that we are building is the mechanization of metatheory and its use in reasoning about programming and specification languages. Such system have been used to address the POPLmark Challenge. An approach to mechanizing metatheory that is related to the perspective we take here can be found in the 2002 ACM ToCL paper by McDowell and Miller (see reference below and the following description of that work).


The principle teams between the six years of funding for Slimmer (2005/2010) were the following two teams.

Two other teams have been added in the final years of this project in order to help shape the next steps to take at the end of the funded period.


Financial support for the project has been obtained from INRIA via its ``Equipes Associées'' program. Matching funds have been contributed by the National Science Foundation (CISE Directorate and the Office of International Science and Engineering, Grant No. 0429572). The opinions, findings, and conclusions or recommendations expressed in this material are those of the project participants and do not necessarily reflect the views of INRIA or the National Science Foundation.



During the six years of its funding, Slimmer provided a context to two PhD thesis (Baelde and Gacek). Several papers were co-authored by members of the associated teams and many other papers were published that contributed to the general thrust of the project. A complete list of publications from this project is available.

Related Sites and Other Relevant Systems