A Framework for Cooperating Decision Procedures. - Clark W. Barrett; David L. Dill; Aaron Stump (CADE, 2000)

A Decision Procedure for an Extensional Theory of Arrays. - Aaron Stump; Clark W. Barrett; David L. Dill; Jeremy R. Levitt (LICS, 2001)

Faster Proof Checking in the Edinburgh Logical Framework. - Aaron Stump; David L. Dill (CADE, 2002)

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. - Clark W. Barrett; David L. Dill; Aaron Stump (CAV, 2002)

CVC: A Cooperating Validity Checker. - Aaron Stump; Clark W. Barrett; David L. Dill (CAV, 2002)

A Generalization of Shostak's Method for Combining Decision Procedures. - Clark W. Barrett; David L. Dill; Aaron Stump (FroCoS, 2002)

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. - Aaron Stump; Clark W. Barrett; David L. Dill (LFM, 2002)

Checking validities and proofs with CVC and flea. - Aaron Stump (2002)

Subset Types and Partial Functions. - Aaron Stump (CADE, 2003)

Foundational proof checkers with small witnesses. - Dinghao Wu; Andrew W. Appel; Aaron Stump (PPDP, 2003)

A Trustworthy Proof Checker. - Andrew W. Appel; Neophytos G. Michael; Aaron Stump; Roberto Virga (J. Autom. Reason., 2003)

Validated Proof-Producing Decision Procedures. - Robert Klapper; Aaron Stump (D/PDPAR@IJCAR, 2004)

Imperative LF Meta-Programming. - Aaron Stump (LFM@IJCAR, 2004)

From Rogue to MicroRogue. - Aaron Stump; Ryan Besand; James C. Brodman; Jonathan Hseu; Bill Kinnersley (WRLA, 2004)

Logical Semantics for the Rewriting Calculus. - Aaron Stump; Carsten Schürmann (STRATEGIES@IJCAR, 2004)

SMT-COMP: Satisfiability Modulo Theories Competition. - Clark W. Barrett; Leonardo Mendonça de Moura; Aaron Stump (CAV, 2005)

A language-based approach to functionally correct imperative programming. - Edwin M. Westbrook; Aaron Stump; Ian Wehrman (ICFP, 2005)

The Algebra of Equality Proofs. - Aaron Stump; Li-Yang Tan (RTA, 2005)

Programming with Proofs: Language-Based Approaches to Totally Correct Software. - Aaron Stump (VSTTE, 2005)

Mining Propositional Simplification Proofs for Small Validating Clauses. - Ian Wehrman; Aaron Stump (PDPAR@CAV, 2005)

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). - Clark W. Barrett; Leonardo Mendonça de Moura; Aaron Stump (J. Autom. Reason., 2005)

Roadmap for enhanced languages and methods to aid verification. - Gary T. Leavens; Jean-Raymond Abrial; Don S. Batory; Michael J. Butler; Alessandro Coglio; Kathi Fisler; Eric C. R. Hehner; Cliff B. Jones; Dale Miller 001; Simon L. Peyton Jones; Murali Sitaraman; Douglas R. Smith; et al. (GPCE, 2006)

Slothrop: Knuth-Bendix Completion with a Modern Termination Checker. - Ian Wehrman; Aaron Stump; Edwin M. Westbrook (RTA, 2006)

Preface. - Aaron Stump; Hongwei Xi 001 (PLPV@IJCAR, 2006)

Knuth-Bendix completion of theories of commuting group endomorphisms. - Aaron Stump; Bernd Löchner (Inf. Process. Lett., 2006)

Lightweight Verification with Dependent Types. - Aaron Stump (VERIFY, 2007)

Signature Compilation for the Edinburgh Logical Framework. - Michael Zeller; Aaron Stump; Morgan Deters (LFMTP@CADE, 2007)

Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). - Clark W. Barrett; Leonardo Mendonça de Moura; Aaron Stump (Formal Methods Syst. Des., 2007)

Proof Checking Technology for Satisfiability Modulo Theories. - Aaron Stump (LFMTP@LICS, 2008)

Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). - Clark W. Barrett; Morgan Deters; Albert Oliveras; Aaron Stump (Int. J. Artif. Intell. Tools, 2008)

The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings. - Edwin M. Westbrook; Aaron Stump; Evan Austin (LFMTP, 2009)

Verified programming in Guru. - Aaron Stump; Morgan Deters; Adam Petcher; Todd Schiller; Timothy W. Simpson (PLPV, 2009)

Directly reflective meta-programming. - Aaron Stump (High. Order Symb. Comput., 2009)

Resource typing in guru: (abstract only). - Aaron Stump; Evan Austin (ACM SIGPLAN Notices, 2009)

Exploring Predictability of SAT/SMT Solvers. - Robert Brummayer; Duckki Oe; Aaron Stump (EMSQMS@IJCAR, 2010)

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). - Clark W. Barrett; Leonardo Mendonça de Moura; Silvio Ranise; Aaron Stump; Cesare Tinelli (Haifa Verification Conference, 2010)

Resource typing in Guru. - Aaron Stump; Evan Austin (PLPV, 2010)

Language-based verification will change the world. - Tim Sheard; Aaron Stump; Stephanie Weirich (FoSER, 2010)

Termination Casts: A Flexible Approach to Termination with General Recursion - Aaron Stump; Vilhelm Sjöberg; Stephanie Weirich (PAR, 2010)

Equality, Quasi-Implicit Products, and Large Eliminations - Vilhelm Sjöberg; Aaron Stump (ITRS, 2010)

Type Preservation as a Confluence Problem. - Aaron Stump; Garrin Kimmell; Roba El Haj Omar (RTA, 2011)

The 2nd Verified Software Competition: Experience Report. - Jean-Christophe Filliâtre; Andrei Paskevich; Aaron Stump (COMPARE, 2012)

Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. - Aaron Stump; Geoff Sutcliffe; Cesare Tinelli (COMPARE, 2012)

Towards typing for small-step direct reflection. - Jacques Carette; Aaron Stump (PEPM, 2012)

Equational reasoning about programs with general recursion and call-by-value semantics. - Garrin Kimmell; Aaron Stump; Harley D. Eades III; Peng Fu 001; Tim Sheard; Stephanie Weirich; Chris Casinghino; Vilhelm Sjöberg; Nathan Collins; Ki Yung Ahn (PLPV, 2012)

LFSC for SMT Proofs: Work in Progress. - Aaron Stump; Andrew Reynolds 001; Cesare Tinelli; Austin Laugesen; Harley Eades III; Corey Oliver; Ruoyu Zhang (PxTP, 2012)

The Design of a Practical Proof Checker for a Lazy Functional Language. - Adam M. Procter; William L. Harrison; Aaron Stump (Trends in Functional Programming, 2012)

versat: A Verified Modern SAT Solver. - Duckki Oe; Aaron Stump; Corey Oliver; Kevin Clancy (VMCAI, 2012)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems - Vilhelm Sjöberg; Chris Casinghino; Ki Yung Ahn; Nathan Collins; Harley D. Eades III; Peng Fu 001; Garrin Kimmell; Tim Sheard; Aaron Stump; Stephanie Weirich (MSFP, 2012)

A Rewriting View of Simple Typing - Aaron Stump; Hans Zantema; Garrin Kimmell; Roba El Haj Omar (Log. Methods Comput. Sci., 2012)

Hereditary Substitution for the λΔ-Calculus. - Harley Eades III; Aaron Stump (COS, 2013)

SMT proof checking using a logical framework. - Aaron Stump; Duckki Oe; Andrew Reynolds 001; Liana Hadarean; Cesare Tinelli (Formal Methods Syst. Des., 2013)

6 Years of SMT-COMP. - Clark W. Barrett; Morgan Deters; Leonardo Mendonça de Moura; Albert Oliveras; Aaron Stump (J. Autom. Reason., 2013)

StarExec: A Cross-Community Infrastructure for Logic Solving. - Aaron Stump; Geoff Sutcliffe; Cesare Tinelli (IJCAR, 2014)

The recursive polarized dual calculus. - Aaron Stump (PLPV, 2014)

Self Types for Dependently Typed Lambda Encodings. - Peng Fu 001; Aaron Stump (RTA-TLCA, 2014)

A lazy approach to adaptive exact real arithmetic using floating-point operations. - Ryan McCleeary; Martin Brain; Aaron Stump (ACM Commun. Comput. Algebra, 2015)

The 2013 Evaluation of SMT-COMP and SMT-LIB. - David R. Cok; Aaron Stump; Tjark Weber (J. Autom. Reason., 2015)

Verified Functional Programming in Agda - Aaron Stump (ACM, 2016)

Project Report: Dependently Typed Programming with Lambda Encodings in Cedille. - Ananda Guneratne; Chad Reynolds; Aaron Stump (TFP, 2016)

Dualized Simple Type Theory. - Harley Eades III; Aaron Stump; Ryan McCleeary (Log. Methods Comput. Sci., 2016)

Efficiency of lambda-encodings in total type theory. - Aaron Stump; Peng Fu 001 (J. Funct. Program., 2016)

The calculus of dependent lambda eliminations. - Aaron Stump (J. Funct. Program., 2017)

Generic derivation of induction for impredicative encodings in Cedille. - Denis Firsov; Aaron Stump (CPP, 2018)

Spine-local Type Inference. - Christopher Jenkins; Aaron Stump (IFL, 2018)

Efficient Mendler-Style Lambda-Encodings in Cedille. - Denis Firsov; Richard Blair; Aaron Stump (ITP, 2018)

From realizability to induction via dependent intersection. - Aaron Stump (Ann. Pure Appl. Log., 2018)

Zero-Cost Coercions for Program and Proof Reuse. - Larry Diehl; Aaron Stump (CoRR, 2018)

Syntax and Semantics of Cedille. - Aaron Stump (CoRR, 2018)

Syntax and Typing for Cedille Core. - Aaron Stump (CoRR, 2018)

Course-of-Value Induction in Cedille. - Denis Firsov; Larry Diehl; Christopher Jenkins; Aaron Stump (CoRR, 2018)

Generic zero-cost reuse for dependent types. - Larry Diehl; Denis Firsov; Aaron Stump (Proc. ACM Program. Lang., 2018)

Quotients by Idempotent Functions in Cedille. - Andrew Marmaduke; Christopher Jenkins; Aaron Stump (TFP, 2019)

Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille. - Christopher Jenkins; Colin McDonald; Aaron Stump (CoRR, 2019)

A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille. - Aaron Stump (LFMTP@LICS, 2019)

Zero-Cost Constructor Subtyping. - Andrew Marmaduke; Christopher Jenkins; Aaron Stump (IFL, 2020)

Efficient lambda encodings for Mendler-style coinductive types in Cedille. - Christopher Jenkins; Aaron Stump; Larry Diehl (MSFP@ETAPS, 2020)

Strong functional pearl: Harper's regular-expression matcher in Cedille. - Aaron Stump; Christopher Jenkins; Stephan Spahn; Colin McDonald (Proc. ACM Program. Lang., 2020)

Simulating Large Eliminations in Cedille. - Christa Jenkins; Andrew Marmaduke; Aaron Stump (TYPES, 2021)

Relational Type Theory (All Proofs). - Aaron Stump; Benjamin Delaware; Christopher Jenkins (CoRR, 2021)

Simulating Large Eliminations in Cedille. - Christopher Jenkins; Andrew Marmaduke; Aaron Stump (CoRR, 2021)

Monotone recursive types and recursive data representations in Cedille. - Christopher Jenkins; Aaron Stump (Math. Struct. Comput. Sci., 2021)

Impredicative Encodings of Inductive-Inductive Data in Cedille. - Andrew Marmaduke; Larry Diehl; Aaron Stump (TFP, 2023)

A Type-Based Approach to Divide-and-Conquer Recursion in Coq. - Pedro Abreu; Benjamin Delaware; Alex Hubers; Christa Jenkins; J. Garrett Morris; Aaron Stump (Proc. ACM Program. Lang., 2023)

Dual counterpart intuitionistic logic. - Anthony Cantor; Aaron Stump (J. Log. Comput., 2024)