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]
2021
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]
2020
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]
2019
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].
2018
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]
2017
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]
2016
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)
2015
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]
2014
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]
2013
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].
2012
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]
2011
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]
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)
2010
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]
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]
Resource Typing in Guru. Aaron Stump and Evan Austin. PLPV 2010.
[PDF], [slides]
2009
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.
2008
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].
2007
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.
2006
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.
"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].
2005
"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.
2004
"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.
2003
"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
"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).
"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.