Publications of Aaron Stump and Collaborators

Slides from some talks are here.

A few short notes are here.

My papers on DBLP.

My profile on Google Scholar.

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

Existing meta-programming languages operate on encodings of programs as data. This paper presents a new meta-programming language, based on an untyped lambda calculus, in which structurally reflective programming is supported directly, without any encoding. The language features call-by-value and call-by-name lambda abstractions, as well as novel reflective features enabling the intensional manipulation of arbitrary program terms. The language is scope safe, in the sense that variables can neither be captured nor escape their scopes. The expressiveness of the language is demonstrated by showing how to implement quotation and evaluation operations, as proposed by Wand. The language's utility for meta-programming is further demonstrated through additional representative examples. A prototype implementation is described and evaluated.

2008

2007

Decision procedures are automated theorem proving algorithms which automatically recognize the theorems of some decidable theory. The correctness of these algorithms is important, since a design error could lead to the misidentification of a false statement as a theorem. In the past, decision procedures have been shown to be correct by mechanically verifying that they are sound, i.e. they only identify valid statements. Soundness does not entail correctness, however, as a decision procedure could still fail to recognize a true formula from the theory it decides. To rigorously verify that a decision procedure for a theory T is correct, it must also be shown to be complete in that it recognize all true propositions from T.

We have developed a decision procedure called Bagahk for the validity of formulas modulo the theory of ground equations T=, which we have proven sound and complete in the proof assistant Coq. In this thesis, we highlight the important lemmas and theorems of these proofs. As part of the soundness proof, we embed Coq-level proof terms into the meta-language of our solver using reflection. As a result of this, Bagahk can also be used to assist users in the construction of other proofs. In addition, we develop a proof system for T= and show that our decision procedure recognizes all T=-provable propositions, showing that Bagahk is complete.

This paper describes the Signature Compiler, which can compile an LF signature to a custom proof checker in either C++ or Java, specialized for that signature. Empirical results are reported showing substantial improvements in proof-checking time over existing LF checkers on benchmarks.

The Satisfiability Modulo Theories Competition (SMT-COMP) arose from the SMT-LIB initiative to spur adoption of common, community-designed formats, and to spark further advances in satisfiability modulo theories (SMT). The first SMT-COMP was held in 2005 as a satellite event of CAV 2005. SMT-COMP 2006 was held August 17 - 19, 2006, as a satellite event of CAV 2006. This paper describes the rules and competition format for SMT-COMP 2006, the benchmarks used, the participants, and the results.

2006

This roadmap describes ways that researchers in four areas -- speci- fication languages, program generation, correctness by construction, and programming languages -- might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas. A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Knuth-Bendix completion is a technique for equational automated theorem proving based on term rewriting. This classic procedure is parametrized by an equational theory and a (well-founded) reduction order used at runtime to ensure termination of intermediate rewriting systems. Any reduction order can be used in principle, but modern completion tools typically implement only a few classes of such orders (e.g., recursive path orders and polynomial orders). Consequently, the theories for which completion can possibly succeed are limited to those compatible with an instance of an implemented class of orders. Finding and specifying a compatible order, even among a small number of classes, is challenging in practice and crucial to the success of the method.

In this thesis, a new variant on the Knuth-Bendix completion procedure is developed in which no order is provided by the user. Modern termination-checking methods are instead used to verify termination of rewriting systems. We prove the new method correct and also present an implementation called Slothrop which obtains solutions for theories that do not admit typical orders and that have not previously been solved by a fully automatic tool.

A Knuth-Bendix completion procedure is parametrized by a reduction ordering used to ensure termination of intermediate and resulting rewriting systems. While in principle any reduction ordering can be used, modern completion tools typically implement only Knuth-Bendix and path orderings. Consequently, the theories for which completion can possibly yield a decision procedure are limited to those that can be oriented with a single path order. In this paper, we present a variant on the Knuth-Bendix completion procedure in which no ordering is assumed. Instead we rely on a modern termination checker to verify termination of rewriting systems. The new method is correct if it terminates; the resulting rewrite system is convergent and equivalent to the input theory. Completions are also not just ground-convergent, but fully convergent. We present an implementation of the new procedure, Slothrop, which automatically obtains such completions for theories that do not admit path orderings.

Knuth-Bendix completions of the equational theories of k greater than or equal to 2 commuting group endomorphisms are obtained, using automated theorem proving and modern termination checking. This improves on modern implementations of completion, where the orderings implemented cannot orient the commutation rules. The result has applications in decision procedures for automated verification.

Dependent types have been proposed for functional programming languages as a means of expressing semantically rich properties as types. In this paper, we consider the problem of bringing semantic programming based on dependent types to an object-oriented language. A type-theoretically light extension to Java (with generics) is proposed, called property types. These are types indexed not by other types (as in Java with generics) but by immutable expressions. We consider programming with two examples of property types: a property type HasFactors< long x, Set a>, expressing that the elements of a are the multiplicative prime factors of x; and a property type Sorted< List l>, expressing that l is sorted.

2005

In this paper a language-based approach to functionally correct imperative programming is proposed. The approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidability of type checking. The methodology used is that of internal verification, where programs manipulate programmer-supplied proofs explicitly as data. The fundamental technical idea of RSP1 is to identify problematic operations as impure, and keep them out of dependent types. The resulting language is powerful enough to verify statically non-trivial properties of imperative and functional programs. The paper presents the ideas through the examples of statically verified merge sort, statically verified imperative binary search trees, and statically verified directed acyclic graphs.

It is by now well known that congruence closure (CC) algorithms can be viewed as implementing ground completion: given a set of ground equations, the CC algorithm computes a convergent rewrite system whose equational theory conservatively extends that of the original set of equations. We call such a rewrite system a CC for the original set. This paper describes work in progress to create an implementation of a CC algorithm which is validated, in the following sense. Any non-aborting, terminating run of the implementation is guaranteed to produce a CC for the input set of equations. Note that aborting or failing to terminate can happen for implementations of CC algorithms only due to bugs in code; the algorithms themselves are usually proved terminating and correct. Validation of an implementation of a CC algorithm is achieved by implementing the algorithm in RSP1, a dependently typed programming language. Type checking ensures that proofs of convergence and conservative extension are well-formed.

The problem of obtaining small conflict clauses in SMT systems has recently received much attention. This paper reports work in progress which aims to obtain small subsets of the current partial assignment that imply the goal formula, in the case when the goal formula has been propositionally simplified under that assignment to true. The approach used is algebraic proof mining. Proofs that the goal is equivalent to true (in the current assignment) are viewed as first-order terms. An equational theory between proofs is then defined, which is sound with respect to the equivalence relation ``proves a theorem in common.'' The theory is completed to obtain a convergent rewrite system that puts proofs into a canonical form. While our canonical form does not use the minimal number of assumptions, it does drop many unnecessary parts of the proof. These unnecessary pieces correspond to the simplifications performed, e.g., on one side of a disjunction whose other side simplifies to true. The paper concludes with speculation on how to obtain a canonical proof with the minimal number of assumptions.

This short paper describes the setup for the Satisfiability Modulo Theories Competition, held as a satellite event of CAV in 2005. See also the SMT-COMP '05 webpage.

Introduced by Peter Andrews in the 1960's, Q0 is a classical higher-order logic based on simply-typed lambda calculus. This paper presents our work in progress on the formalizing of Q0 in a programming language, Rogue-Sigma-Pi (RSP), with the aim of validating its meta-theory. The main challenge of this project arises from the fact that while all logical derivations are carried out in much detail in Andrews' formalism, many of the syntactic derivations have been kept implicit. Therefore, most of our work has been devoted to setting up a framework that allows us to formalize low-level syntactic notions of Q0, such as variable occurrences, bindings and replacement. This formalization also includes proving meta-theoretic properties of these various syntactic notions. Building on the the ability to prove syntactic derivations assumed in Andrews' formalism, recent progress has led to the proving of basic meta-theorems of Q0, such as the equality rules, alpha-equivalence, beta- and eta-conversions, as well as capture-avoiding substitution. This paper will discuss the theoretical and engineering challenges faced in our formalizing of Q0 in RSP that is guided by a faithful adherence to Andrews' presentation on paper.

The Edinburgh Logical Framework (LF) has been proposed as a system for expressing inductively defined sets. I will present an inductive definition of the set of manifold meshes in LF. This definition takes into account the topological characterization of meshes, namely their Euler Characteristic. I will then present a set of dependent data types based on this inductive definition. These data types are defined in a programming language based on LF. The language's type checking guarantees that any typeable expression represents a correct manifold mesh. Furthermore, any mesh can be represented using these data types. Hence, the encoding is sound and complete.

Proofs of equalities may be built from assumptions using proof rules for reflexivity, symmetry, and transitivity. Reflexivity is an axiom proving x=x for any x; symmetry is a 1-premise rule taking a proof of x=y and returning a proof of y=x; and transitivity is a 2-premise rule taking proofs of x=y and y=z, and returning a proof of x=z. Define an equivalence relation to hold between proofs iff they prove a theorem in common. The main theoretical result of the paper is that if all assumptions are independent, this equivalence relation is axiomatized by the standard axioms of group theory: reflexivity is the unit of the group, symmetry is the inverse, and transitivity is the multiplication. Using a standard completion of the group axioms, we obtain a rewrite system which puts equality proofs into canonical form. Proofs in this canonical form use the fewest possible assumptions, and a proof can be canonized in linear time using a simple strategy. This result is applied to obtain a simple extension of the union-find algorithm for ground equational reasoning which produces minimal proofs. The time complexity of the original union-find operations is preserved, and minimal proofs are produced in worst-case time $O(n^{\textit{log}_2 3})$, where $n$ is the number of expressions being equated. As a second application, the approach is used to achieve significant performance improvements for the CVC cooperating decision procedure.

2004

The Rewriting Calculus has been proposed as a language for defining term rewriting strategies. Rules are explicitly represented as terms, and are applied explicitly to other terms to transform them. Sets of rules may be applied to (sets of) terms non-deterministically to obtain sets of results. Strategies are implemented as rules which accept other rules as arguments and apply them in certain ways. This paper describes work in progress to strengthen the Rewriting Calculus by giving it a logical semantics. Such a semantics can provide crucial guidance for studying the language and increasing its expressive power. The latter is demonstrated by adding support to the Rewriting Calculus for what we call \emph{higher-form rewriting}, where rules rewrite other rules. The logical semantics used is based on ordered linear logic. The paper develops the ideas through several examples.

A widely used technique to integrate decision procedures (DPs) with other systems is to have the DPs emit proofs of the formulas they report valid. One problem that arises is debugging the proof-producing code; it is very easy in standard programming languages to write code which produces an incorrect proof. This paper demonstrates how proof-producing DPs may be implemented in a programming language, called Rogue-Sigma-Pi (RSP), whose type system ensures that proofs are manipulated correctly. RSP combines the Rogue rewriting language and the Edinburgh Logical Framework (LF). Type-correct RSP programs are partially correct: essentially, any putative LF proof object produced by a type-correct RSP program is guaranteed to type check in LF. The paper describes a simple proof-producing combination of propositional satisfiability checking and congruence closure implemented in RSP.

Logical frameworks have enjoyed wide adoption as meta-languages for describing deductive systems. While the techniques for representing object languages in logical frameworks are relatively well understood, languages and techniques for meta-programming with them are much less so. This paper presents work in progress on a programming language called Rogue-Sigma-Pi (RSP), in which general programs can be written for soundly manipulating objects represented in the Edinburgh Logical Framework (LF). The manipulation is sound in the sense that, in the absence of runtime errors, any putative LF object produced by a well-typed RSP program is guaranteed to type check in LF. An important contribution is an approach for soundly combining imperative features with higher-order abstract syntax. The focus of the paper is on demonstrating RSP through representative LF meta-programs.

The Rewriting Calculus has been proposed as a foundational system combining the central ideas of lambda-calculus and term rewriting. The rewriting is explicit, in the sense that rules must be applied explicitly to terms to transform them. This paper begins with an imperative version of the Rewriting Calculus called Rogue. It then shows how Rogue can itself be conveniently implemented by an even more foundational system called MicroRogue. MicroRogue rewrites terms using a global set of first-order rules. Rules can be enabled, disabled, and dynamically added in scopes, which can be pushed and popped. MicroRogue also provides mechanisms for specifying evaluation order. Using these primitives, a Rogue interpreter can be implemented in less than 40 lines of MicroRogue code.

2003

Efficient decision procedures require a substantial engineering effort to implement in mainstream languages. This paper proposes a new programming language called Rogue for implementing decision procedures. Rogue is a rewriting language with backtrackable mutable expression attributes and an interface to a fast SAT solver. Work in progress on implementing a Nelson-Oppen style cooperating validity checker in Rogue is also briefly described.

A classical higher-order logic PFsub of partial functions is defined. The logic extends a version of Farmer's logic PF by enriching the type system of the logic with subset types and dependent types. Validity in PFsub is then reduced to validity in PF by a translation.

Older Works

- "Foundational Proof Checkers with Small
Witnesses", Dinghao Wu, Andrew Appel, and Aaron Stump, at PPDP, 2003 (abstract, gzipped PostScript).

- "A Trustworthy Proof Checker", Andrew
W. Appel, Neophytos G. Michael, Aaron Stump, and Roberto Virga,
Journal of Automated Reasoning, Volume 31, pages 231-260, 2003,
special issue on proof-carrying code. Revised version of earlier paper.

- "CVC: a Cooperating Validity Checker", Aaron Stump, Clark
W. Barrett, and David L. Dill, system description at CAV 2002 (abstract,
gzipped PostScript).

- "Faster Proof Checking in the Edinburgh
Logical Framework", Aaron Stump and David L. Dill, at CADE-18 (abstract, gzipped PostScript).

- "Checking Satisfiability of First-Order
Formulas by Incremental Translation to SAT", Clark W. Barrett, David
L. Dill, and Aaron Stump, at CAV 2002 (abstract, Bibtex,
gzipped PostScript,
PDF).

- "A Trustworthy Proof Checker", Andrew
W. Appel, Neophytos G. Michael, Aaron Stump, and Roberto Virga, at the
FCS-VERIFY '02 workshops' joint session. Available as a Princeton
tech report.

- "Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF", Aaron Stump, Clark Barrett, and David Dill, at LFM 2002 (Bibtex, PDF).

- "A Generalization of Shostak's Method for
Combining Decision Procedures ", Clark W. Barrett, David L. Dill, and
Aaron Stump, at FroCos '02 (abstract, Bibtex,
gzipped PostScript).

- "A Decision Procedure for an Extensional Theory of Arrays", Aaron
Stump, Clark W. Barrett, David L. Dill, and Jeremy Levitt. LICS '01 (abstract, gzipped PostScript, Bibtex, slides for talk given at
LICS'01).

- "A Framework for Cooperating Decision Procedures", Clark
W. Barrett, David L. Dill and Aaron Stump, at CADE-17, June 2000 (abstract, Bibtex, gzipped
PostScript). [LNCS]

- "Generating Proofs from a Decision Procedure", Aaron Stump
and David L. Dill, in the FLoC '99 workshop
on Run-Time Result
Verification (gzipped
PostScript).

Other works

- "Checking Validities and Proofs with CVC and
flea", Aaron Stump, Ph.D. thesis, Stanford University, August 2002 (gzipped Postscript).

- "On Coquand's `An Analysis of Girard's Paradox'", Aaron Stump, written portion of MTC qualifying exam, spring 1999 (gzipped PostScript). Also, see the source code for several different formal systems I implemented in Twelf as an exercise in preparing for this qual.

Return to my home page.