SLIMMER:
Sophisticated Logic Implementations for Modeling and Mechanical Reasoning
The SLIMMER project is currently 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
implication 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 may be useful in addressing 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).
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.
-
The Abella system was released
in February 2008. This is an interactive theorem prover for proving
properties of specifications written in the second-order hereditary
Harrop formula logic. The meta-reasoning is based on an extension of
the Alwen Tiu's LG-omega logic. The details of this extended logic are
available in a recently submitted
paper. Abella is written in OCaml by
Andrew Gacek and uses the higher-order pattern unification code of
Gopalan Nadathur and Natalie Linnell.
-
Version 1.1 of Bedwyr was released in February
2007 (following the initial release of Version 1.0 in November 2006).
This open source system is hosted on INRIA's GForge system under the
Slimmer project.
This OCaml system was developed by David Baelde and Andrew Gacek with
help from Axelle Ziegler and code for pattern unification code
extracted from the Teyjus system. Read more.
-
Version 0.9.2 of the Tac system was released in January
2010. This open source system is hosted on INRIA's GForge system under the
Slimmer project as
well. This OCaml system was developed by David Baelde, Zach Snow, and
Alexandre Viel. Read more.
-
Gopalan Nadathur and Natalie Linnell (University of Minnesota) have
posted their code
for An implementation of Higher-Order Pattern Unification in SML.
-
Alwen Tiu's SML code for the Level
0/1 prover. This system has largely been superseded by the Bedwyr
system.
Below is a list of publications, listed in chronological order, that
are most related to the Slimmer effort.
-
Raymond McDowell and Dale Miller,
Reasoning with Higher-Order
Abstract Syntax in a Logical Framework, ACM Transactions on
Computational Logic, 3(1) (January 2002), 80 - 136 (
pdf). An early reference for mechanizing
the meta-theory of simple programming languages.
Alwen Tiu,
A Logical Framework for Reasoning about Logical
Specifications, PhD, Pennsylvania State University, May 2004. (
pdf).
This thesis presents the LINC logic that is behind much of this effort.
Gopalan Nadathur and Xiaochu Qi,
Optimizing the Runtime Processing
of Types in a Higher-Order Logic Programming Language. LPAR'05. (
PDF,
PS)
Gopalan Nadathur and Natalie Linnell,
Practical Higher-Order
Pattern Unification With On-the-Fly Raising, ICLP'05 (
PDF,
PS). The algorithms and code described in this system play an
important role in our implemented systems.
Dale Miller and Alwen Tiu,
A Proof Theory for Generic
Judgments. ACM Transactions on
Computational Logic, 6(4), pp. 749--783, October 2005.
(
dvi,
ps,
pdf). The first comprehensive account
of the ∇-quantifier.
Alwen Tiu and Gopalan Nadathur and Dale Miller,
Mixing Finite
Success and Finite Failure in an Automated Prover.
In
Proceedings of ESHOL'05: Empirically Successful Automated
Reasoning in Higher-Order Logics, pages 79 - 98, December 2005.
(
pdf)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and
Alwen Tiu.
A User Guide to Bedwyr, November 2006.
[
bib |
.pdf ]
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and
Alwen Tiu.
The Bedwyr system for model checking over syntactic
expressions
CADE 2007: 21th Conference on Automated Deduction, LNAI
4603, pages 391-397. Springer, 2007. (
pdf)
- Abella -
an interactive theorem prover using higher-order abstract
syntax and the ∇-quantifier.
-
Bedwyr - a model checker using higher-order abstract
syntax and the ∇-quantifer.
- Tac - an interactive theorem prover.
- λProlog
- a higher-order logic programming language
- Teyjus - An implementation
of Lambda Prolog
-
LINC - Including the Level 0/1 Prover (the predecessor
of the Bedwyr system).
Bedwyr V1.0 was announced on various mailing lists on 1 Nov 2006.
Nadathur described the foundations and architecture of the system
(actually, an earlier prototype) at ESHOL'05 in December 2005. Miller gave a short
presentation on Bedwyr at CSFW'06. Baelde presented
a paper on Bedwyr in June 2007 at CADE-21. Bedwyr V1.1 was released
15 February 2007.
During June
2006 and June
2007, a number of researchers visited LIX in France to discuss a
number of topics. A prominent theme during these months concerned
the Slimmer project.
During 26-28 May 2007, Baelde, Miller, and Tiu presented their
work related to Slimmer at the workshop on Mathematical Theories of
Abstraction, Substitution and Naming in Computer Science at ICMS in
Edinburgh.
During 30 June - 1 July 2005, Gacek and Nadathur organized
WIPS 2005: Workshop on
Implementations of Proof Search at the Digital Technology Center at the
University of Minnesota.
Several exchanges of people between the University of Minnesota, LIX,
and Canberra, Australia have taken place. Only visits of longer than
a week are listed below.
- 19 June - 3 July 2007: Gopalan Nadathur visited LIX and
attended talks at RDP 2007 in Paris.
- 15 May - 31 July 2007 : Zach Snow, a graduate student at the
University of Minnesota, was an intern at LIX.
- October 2006 :
David Baelde visited Alwen Tiu in Canberra Australia for most of the month.
- June-July 2006 :
Andrew Gacek, a graduate student at the University of Minnestoa,
was an intern at LIX for two months.
- June 2006 :
Alwen Tiu, from ANU, visited LIX for the two weeks.
- May 13-25, 2006 :
David Baelde, a graduate student at LIX/Ecole Polytechnique, visited
the University of Minnesota for two weeks.