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.


Dual Counterpart Intuitionistic Logic, Anthony Cantor, Aaron Stump. Journal of Logic and Computation. In press. [PDF]

Impredicative Encodings of Inductive-Inductive Data in Cedille, Andrew Marmaduke, Larry Diehl, Aaron Stump. Trends in Functional Programming. 24th International Symposium on Trends in Functional Programming (TFP), Springer Lecture Notes in Computer Science, volume 13868, pages 1-15. Best student paper award. [PDF]

A Type-Based Approach to Divide-And-Conquer Recursion in Coq, Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump. Proceedings of the ACM on Programming Languages, Principles of Programming Languages (POPL). Full citation information not available yet. [PDF]


Monotone Recursive Types and Recursive Data Representations in Cedille, Christa Jenkins and Aaron Stump. Mathematical Structures in Computer Science, volume 31, number 6, pages 682-745. [PDF]

Simulating Large Eliminations in Cedille, Christa Jenkins, Andrew Marmaduke, and Aaron Stump. TYPES 2021 post-proceedings, LIPIcs volume 239, pages 9:1 - 9:22. doi 10.4230/LIPIcs.TYPES.2021.9 . [PDF]


Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille, Aaron Stump, Christa Jenkins, Stephan Spahn, Colin McDonald. International Conference on Functional Programming (ICFP), published in PACMPL, doi 10.1145/3409004, [PDF]

Zero-Cost Constructor Subtyping, Andrew Marmaduke, Christa Jenkins, Aaron Stump. Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages (IFL) [PDF].

Efficient lambda encodings for Mendler-style coinductive types in Cedille, Christa Jenkins, Aaron Stump, Larry Diehl. Proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP) [PDF]


A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille, Aaron Stump. Electronic Proceedings in Theoretical Computer Science (EPTCS), volume 307, pages 55-67 [PDF]

Quotients by Idempotent Functions in Cedille, Andrew Marmaduke, Christa Jenkins, Aaron Stump. Proceedings of the 20th International Symposium on Trends in Functional Programming (TFP) [PDF].


Spine-local type inference, Christa Jenkins and Aaron Stump. Proceedings of the 30th Symposium on Implementation and Application of Functional Languages (IFL) [PDF].

Generic Zero-Cost Reuse for Dependent Types, Larry Diehl, Denis Firsov, and Aaron Stump. International Conference on Functional Programming (ICFP) [PDF]

Efficient Mendler-Style Lambda-Encodings in Cedille, Denis Firsov, Richard Blair, and Aaron Stump. Interactive Theorem Proving (ITP) [PDF]

Generic Derivation of Induction for Impredicative Encodings in Cedille, Denis Firsov and Aaron Stump. Certified Programs and Proofs (CPP) [PDF]

From Realizability to Induction via Dependent Intersection Aaron Stump. Annals of Pure and Applied Logic 169(7), pages 637-655. [PDF]


The Calculus of Dependent Lambda Eliminations. Aaron Stump. Journal of Functional Programming, volume 27, e14 [PDF] [version with all proofs]

Project Report: Dependently typed programming with lambda encodings in Cedille.Ananda Guneratne, Chad Reynolds, and Aaron Stump. Trends in Functional Programming 2016, post-proceedings paper (accepted 2017). [PDF]


Dualized Simple Type Theory. Harley Eades III, Aaron Stump, and Ryan McCleeary. Logical Methods in Computer Science, volume 12, issue 3, pages 1-47. [PDF]

Efficiency of Lambda-Encodings in Total Type Theory. Aaron Stump and Peng Fu. Journal of Functional Programming, 26:e2. [PDF] (this version corrects a typo in the definition of CexpR)


The 2013 Evaluation of SMT-COMP and SMT-LIB. David Cok, Aaron Stump, and Tjark Weber. Journal of Automated Reasoning, Volume 55 Issue 1, June 2015, pages 61-90 [PDF]


Self Types for Dependently Typed Lambda Encodings. Peng Fu and Aaron Stump. Rewriting Techniques and Applications/Typed Lambda Calculi and Applications (RTA-TLCA 2014 joint conference) [PDF (this is the extended version with all proofs)].

StarExec: a Cross-Community Infrastructure for Logic Solving. Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. International Joint Conference on Automated Reasoning (IJCAR '14) [PDF].

The Recursive Polarized Dual Calculus. Aaron Stump. Programming Languages meets Program Verification (PLPV) [PDF].

The Semantic Analysis of Advanced Programming Languages. Harley Eades III, doctoral dissertation, The University of Iowa . [PDF].

Lambda Encodings in Type Theory. Peng Fu, doctoral dissertation, The University of Iowa. [PDF]


Extended Abstract: Reconsidering Intuitionistic Duality. Aaron Stump, Harley Eades III, Ryan McCleeary. Workshop on Control Operators and their Semantics (COS 2013). [PDF, extended version with proofs]

Hereditary Substitution for the Lambda-Delta-Calculus. Harley Eades and Aaron Stump. EPTCS 127, 2013, pp. 45-65. [PDF, on arXiv]

Equational Reasoning about Programs with General Recursion and Call-by-value Semantics. Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn. Progress in Informatics, No. 10, March 2013, pages 19-46. Journal version of PLPV '12 paper. [PDF]

6 Years of SMT-COMP. Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras, Aaron Stump. Journal of Automated Reasoning, volume 50, number 3, pages 243-277. [PDF]

SMT Proof Checking Using a Logical Framework. Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. volume 42, number 1, pages 91-118, 2013. [preprint PDF].


A Rewriting View of Simple Typing. Aaron Stump, Hans Zantema, Garrin Kimmell, Ruba El Haj Omar. Logical Methods in Computer Science, available on arXiv as of November 2012. [PDF].

Formally Certified Satisfiability Solving. Duckki Oe, doctoral thesis, August, 2012, The University of Iowa [PDF]

The 2nd Verified Software Competition: Experience Report. Jean-Christophe Filliatre, Andrei Paskevich, and Aaron Stump. 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012), 2012. [PDF]

versat: A Verified Modern SAT Solver. Duckki Oe, Aaron Stump, Corey Oliver, and Kevin Clancy. VMCAI 2012. [PDF]

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems. Vilhelm Sjoeberg,Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich. MSFP 2012. [PDF]

Equational Reasoning about Programs with General Recursion and Call-by-value Semantics. Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn. PLPV 2012. [PDF]

Towards Typing for Small-Step Direct Reflection. Jacques Carette and Aaron Stump. PEPM '12. [PDF]


A Framework for Internalizing Relations into Type Theory. Peng Fu, Aaron Stump, and Jeff Vaughan. PSATTT 2011. [PDF]

Extended Abstract: Combining a Logical Framework with an RUP Checker for SMT Proofs. Duckki Oe and Aaron Stump. SMT 2011. [PDF]

Blaise Compiler. Austin Laugesen, undergraduate honor's thesis. [PDF]

Type Preservation as a Confluence Problem. Aaron Stump, Garrin Kimmell, and Ruba El Haj Omar. This paper received the best paper award at RTA 2011. [PDF] (long version with proofs)


Language-Based Verification Will Change the World. Tim Sheard, Aaron Stump, Stephanie Weirich. Position paper at Future of Software Engineering Research (FoSER) working conference. [PDF]

Comparing Proof Systems for Linear Real Arithmetic with LFSC. Andrew Reynolds, Liana Haderean, Cesare Tinelli, Yeting Ge, Aaron Stump, Clark Barrett. SMT-2010, a FLoC workshop. [PDF]

The SMT-LIB Standard -- Version 2.0. Clark Barrett, Aaron Stump, Cesare Tinelli. SMT-2010, a FLoC workshop. [PDF, see also the full reference manual (PDF)]

Hereditary Substitution for Stratified System F. Harley Eades III, Aaron Stump. PSTT-2010, a FLoC workshop. [PDF]

Exploring Predictability of SAT/SMT Solvers. Robert Brummayer, Duckki Oe, and Aaron Stump. EMSQMS-2010, a FLoC workshop. [PDF]

Termination Casts: a Flexible Approach to Termination with General Recursion. Aaron Stump, Vilhelm Sjoeberg, and Stephanie Weirich. PAR-2010, a FLoC workshop. [PDF]

Equality, Quasi-Implicit Products, and Large Eliminations. Vilhelm Sjoeberg and Aaron Stump. ITRS-2010, a FLoC workshop. [PDF, long version with all proofs]

Resource Typing in Guru. Aaron Stump and Evan Austin. PLPV 2010. [PDF], [slides]


The Calculus of Nominal Inductive Constructions. Edwin Westbrook, Aaron Stump, Evan Austin. Logical Frameworks and Meta-languages: Theory and Practice (LFMTP). [PDF].

Fast and Flexible Proof Checking for SMT. Duckki Oe, Andrew Reynolds, and Aaron Stump. Satisfiability Modulo Theories (SMT). [PDF].

Deciding Joinability Modulo Ground Equations in Operational Type Theory. Adam Petcher and Aaron Stump. Proof Search in Type Theories (PSTT). [PDF].

Verified Programming in Guru. Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, and Timothy Simpson. Programming Languages meets Program Verification (PLPV), 2009. [PDF].

Verified Programming in Guru. Aaron Stump. Unpublished notes, 2009. [PDF].

Directly Reflective Meta-Programming. Aaron Stump. The journal of Higher Order and Symbolic Computation, volume 22, number 2, pages 115-144, 2009. [PDF]. The version here fixes a bug reported to me by John Clements. Implementation and examples are here.

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.


Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007). Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump. International Journal of Artificial Intelligence Tools (IJAIT), Volume 17, number 4. [PDF]

Higher-Order Encodings with Constructors. Edwin Westbrook. Doctoral Dissertation, Washington University in St. Louis, December 2008. [PDF]

Towards an SMT Proof Format. Aaron Stump and Duckki Oe. In proceedings of the International Workshop on Satisfiability Modulo Theories (SMT), 2008. [PDF]

Proof Checking Technology for Satisfiability Modulo Theories. Aaron Stump. In proceedings of the International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), 2008. [PDF]

Deciding Joinability Modulo Ground Equations in Operational Type Theory. Adam Petcher. Master's Thesis, Washington University in St. Louis, April 2008. [PDF]

Verified Translation to Directional Combinators. Megan Bailey, undergraduate research project report, May 2008.[PDF].


Baghak: Developing Sound and Complete Decision Procedures in Coq. Benjamin Delaware. Master's Thesis, Washington University in St. Louis, August 2007. [PDF]

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.

A Signature Compiler for the Edinburgh LF. Michael Zeller, Aaron Stump, and Morgan Deters; International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007). [PDF]

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.

Design and Results of the 2nd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2006). Clark Barrett, Leonardo de Moura, and Aaron Stump. Formal Methods in System Design, volume 31, number 3, pages 221-239. [PDF]

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.


Roadmap for Enhanced Languages and Methods to Aid Verification. Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler, Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, and Aaron Stump. Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06 2006, Pages 221-236. Also Department of Computer Science, Iowa State University, TR #06-21, July 2006. [PDF]

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 with Modern Termination Checking, Ian Wehrman, Master's Thesis, Washington University in St. Louis, August 2006. Expanded version of RTA 2006 paper below with the same title. [PDF].

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.

Slothrop: Knuth-Bendix Completion with a Modern Termination Checker, Ian Wehrman, Aaron Stump, Edwin Westbrook; International Conference on Rewriting Techniques and Applications (RTA) [PDF].

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.

Free Variable Types, Edwin Westbrook; Trends in Functional Programming (TFP), April 2006. [PDF]

"Knuth-Bendix Completion of Theories of Commuting Group Endomorphisms", Aaron Stump and Bernd Loechner, Information Processing Letters, Volume 98, Issue 5, pages 195-198. [PDF]

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.

"POPLmark 1a with Named Bound Variables", Aaron Stump, presented at an informal workshop on the POPLmark challenge, January 2006, following POPL. [PDF] [Coq proofs].

"Property Types: Semantic Programming for Java", Aaron Stump and Ian Wehrman, Foundations and Developments of Object-Oriented Languages (FOOL/WOOD), January, 2006, affiliated with POPL 2006. [PDF] [BIB]. [Examples from the paper]

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.

"Design and Results of the 1st Satisfiability Modulo Theories Competition (SMT-COMP 2005)", Clark Barrett, Leonardo de Moura, and Aaron Stump; the Journal of Automated Reasoning, Volume 35, pages 373-390 [PDF].


"Programming with Proofs: Language-Based Approaches to Totally Correct Software", Aaron Stump; invited position paper at IFIP working group conference on "Verified Software: Theories, Tools, Experiments" [PDF (slightly revised May 31, 2006] [BIB].

"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].

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.

"Validated Construction of Congruence Closures", Aaron Stump; the CADE Workshop on Disproving [PDF] [BIB].

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.

"Mining Propositional Simplification Proofs for Small Validating Clauses", Ian Wehrman and Aaron Stump; the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning [PDF] [BIB]. Note that the PDF corrects an omission in Appendix B of the original paper, by including some additional equations which are needed for a ground-convergent reduction system.

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.

"SMT-COMP: Satisfiability Modulo Theories Competition", Clark Barrett, Leonardo de Moura, Aaron Stump; 17th International Conference on Computer-Aided Verification (CAV), short paper [PDF] [BIB], short talk at CAV '05 [PDF].

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.

"Formalizing the Meta-Theory of Q0 in Rogue-Sigma-Pi", Li-Yang Tan, 17th European Summer School in Logic, Language, and Information (ESSLLI), student session, 2005 [PDF].

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.

"What a Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms", Joel Brandt, Master's Thesis, April 2005. [PDF], [BIB]

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.

"The Algebra of Equality Proofs", Aaron Stump and Li-Yang Tan, at RTA 2005. [PDF], [BIB]

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.


"Logical Semantics for the Rewriting Calculus", Aaron Stump and Carsten Schuermann, at the 5th International Workshop on Strategies in Automated Deduction (STRATEGIES 04). [PS (revised January 31, 2005)],[BIB]

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.

"Validated Proof-Producing Decision Procedures", Robert Klapper and Aaron Stump, at PDPAR 04. [PS], [BIB]

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.

"Imperative LF Meta-Programming", Aaron Stump, at the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 04), 2004. [PS], [BIB]

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.

"From Rogue to MicroRogue", Aaron Stump, Ryan Besand, James Brodman, Jonathan Hseu, and Bill Kinnersley, 5th International Workshop on Rewriting Logic and Applications (affiliated with ETAPS), 2004. [PS], [BIB]

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.


"Rogue Decision Procedures", Aaron Stump, Arun Deivanayagam, Spencer Kathol, Dylan Lingelbach, and Daniel Schobel, 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), 2003. [PS], [BIB]

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.

"Subset Types and Partial Functions", Aaron Stump, at CADE-19, 2003. This is an extended version with some corrections, modified 7/24/03. [PS], [PDF], [BIB]

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

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

  2. "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.

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

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

  5. "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).

  6. "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.

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

  8. "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).

  9. "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).

  10. "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]

  11. "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

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

  2. "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.