Computational Logic Group
The Computational Logic Group at Washington University studies topics at the
intersection of Computer Science and Logic. Our work combines theory
and engineering: we design formal systems, prove things about them,
and develop implementations. Our work falls into four main
areas: language-based approaches to program verification; decision
procedures; type theory and logical frameworks; and term rewriting.
The first two areas are currently supported by two National Science
Foundation grants. Other activities associated with the group include
the Programming Languages meets Program Verification Workshop (PLPV) and the Satisfiability Modulo
Theories Competition (SMT-COMP).
Language-based Approaches
to Program Verification
We are pursuing language-based approaches to the problem of static
verification of general properties of programs. In the spirit of
Martin-Loef type theory, we want to write programs that accept proofs
(reified as data in the programming language) of their pre-conditions
as input, and produce proofs of their post-conditions as output. The
group is exploring the rich and relatively unexplored design space
in this area through several different languages and language fragments:
- Guru: The core technical features are a primitive, untyped
equality; introduction of equalities at pattern-matching points; a
weak definitional equality relation that does not include arbitrary
conversion; explicit (inductive) proof terms to justify type
coercions; and a separation of proofs and programs that allows
impredicative polymorphism for programs only (not for proofs).
A preliminary implementation is available here.
- Archon: This is a new language supporting directly
reflective meta-programming, and designed for verification. A draft
paper and prototype implementation are available on the Archon page.
- RSP: This is an early language design for programming
with dependent types (superceded now by Guru). RSP has
term-indexed user-declared datatypes, dependent function and record
types, and imperative features. The meta-theory of RSP, and several
examples of imperative programming with dependent types, are studied
in the paper
"A Language-based Approach to Functionally Correct
Imperative Programming", Edwin Westbrook, Aaron Stump, Ian Wehrman;
the 10th ACM SIGPLAN International Conference on Functional
Programming (ICFP) [PDF]
[BIB]
[Tech Report].
- Free variable types: Edwin Westbrook has devised a type
systems tracking occurrence of free variables, in order to support
dependently typed programming with higher-order abstract syntax. See
the paper
Free Variable Types, Edwin Westbrook;
Trends in Functional
Programming (TFP), April 2006. [PDF]
Type Theory and
Logical Frameworks
We have collaborated with Andrew Appel on trustworthy,
high-performance proof checking in the context of foundational
proof-carrying code (see the co-authored papers here). More
recently, we have implemented a signature compiler for LF,
which compiles LF signatures to C++ or Java code for proof checkers
specialized for the signature. The implementation and a draft paper
are available here.
We have also developed a partial solution to the POPLmark challenge
(see here), and have worked through some
ideas in Coq on contextual term interpretations for reducing the
burden of proof for programming languages metatheory (see here).
Term Rewriting
Together with Carsten Schuermann, we have looked at semantics for the
Rewriting Calculus devised by Cirstea and Kirchner. We have also
studied the algebra of equality proofs, which turn out to behave like
terms in the theory of free groups (with congruence rules, we get the
theory of free groups with commuting endomorphisms). Ian
Wehrman has implemented a Knuth-Bendix completion procedure based on
modern termination methods (existing completion tools rely just on
classic termination methods based on simplification orderings like the
Knuth-Bendix ordering or the lexicographic path ordering). See his Slothrop
web page.
Decision
Procedures
In automated reasoning, decision procedures are programs that
can determine whether or not a logical formula is valid, possibly with
respect to some background theory like arithmetic. Most work on
decision procedures either tries to decide logics or logical theories
which were not previously decided, or to decide such (or some special
cases) more efficiently than was previously possible.
Our main recent efforts in decision procedures have been implementing
partially verified cooperating decision procedures. After investing
substantial effort into doing this in RSP, we have switched gears and
are working in Coq. Ben Delaware currently has a simple validity
checker for classical propositional logic plus equalities between
ground atoms written in Coq and proved sound and complete.
See Aaron Stump's research statement for
a more comprehensive discussion of some of the group's work.