Aaron Stump

Publication Activity (10 Years)

Years Active: 2000-2024
Publications (10 Years): 30

Top Topics

Data Representations

Intuitionistic Logic

Experiential Knowledge

Top Venues

Proc. ACM Program. Lang.

J. Funct. Program.

Publications

Anthony Cantor, Aaron Stump
Dual counterpart intuitionistic logic. J. Log. Comput. 34 (3) (2024)
Andrew Marmaduke, Larry Diehl, Aaron Stump
Impredicative Encodings of Inductive-Inductive Data in Cedille. TFP (2023)
Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump
A Type-Based Approach to Divide-and-Conquer Recursion in Coq. Proc. ACM Program. Lang. 7 (POPL) (2023)
Christa Jenkins, Andrew Marmaduke, Aaron Stump
Simulating Large Eliminations in Cedille. TYPES (2021)
Christopher Jenkins, Andrew Marmaduke, Aaron Stump
Simulating Large Eliminations in Cedille. CoRR (2021)
Aaron Stump, Benjamin Delaware, Christopher Jenkins
Relational Type Theory (All Proofs). CoRR (2021)
Christopher Jenkins, Aaron Stump
Monotone recursive types and recursive data representations in Cedille. Math. Struct. Comput. Sci. 31 (6) (2021)
Christopher Jenkins, Aaron Stump, Larry Diehl
Efficient lambda encodings for Mendler-style coinductive types in Cedille. MSFP@ETAPS (2020)
Andrew Marmaduke, Christopher Jenkins, Aaron Stump
Zero-Cost Constructor Subtyping. IFL (2020)
Aaron Stump, Christopher Jenkins, Stephan Spahn, Colin McDonald
Strong functional pearl: Harper's regular-expression matcher in Cedille. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Christopher Jenkins, Aaron Stump
Monotone recursive types and recursive data representations in Cedille. CoRR (2020)
Andrew Marmaduke, Christopher Jenkins, Aaron Stump
Quotients by Idempotent Functions in Cedille. TFP (2019)
Christopher Jenkins, Colin McDonald, Aaron Stump
Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille. CoRR (2019)
Aaron Stump
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille. LFMTP@LICS (2019)
Christopher Jenkins, Aaron Stump
Spine-local Type Inference. CoRR (2018)
Aaron Stump
From realizability to induction via dependent intersection. Ann. Pure Appl. Log. 169 (7) (2018)
Denis Firsov, Larry Diehl, Christopher Jenkins, Aaron Stump
Course-of-Value Induction in Cedille. CoRR (2018)
Larry Diehl, Denis Firsov, Aaron Stump
Generic Zero-Cost Reuse for Dependent Types. CoRR (2018)
Denis Firsov, Richard Blair, Aaron Stump
Efficient Mendler-Style Lambda-Encodings in Cedille. CoRR (2018)
Larry Diehl, Denis Firsov, Aaron Stump
Generic zero-cost reuse for dependent types. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Aaron Stump
Syntax and Typing for Cedille Core. CoRR (2018)
Larry Diehl, Aaron Stump
Zero-Cost Coercions for Program and Proof Reuse. CoRR (2018)
Denis Firsov, Richard Blair, Aaron Stump
Efficient Mendler-Style Lambda-Encodings in Cedille. ITP (2018)
Denis Firsov, Aaron Stump
Generic derivation of induction for impredicative encodings in Cedille. CPP (2018)
Aaron Stump
Syntax and Semantics of Cedille. CoRR (2018)
Christopher Jenkins, Aaron Stump
Spine-local Type Inference. IFL (2018)
Aaron Stump
The calculus of dependent lambda eliminations. J. Funct. Program. 27 (2017)
Ananda Guneratne, Chad Reynolds, Aaron Stump
Project Report: Dependently Typed Programming with Lambda Encodings in Cedille. TFP (2016)
Harley Eades III, Aaron Stump, Ryan McCleeary
Dualized Simple Type Theory. Log. Methods Comput. Sci. 12 (3) (2016)
Aaron Stump, Peng Fu
Efficiency of lambda-encodings in total type theory. J. Funct. Program. 26 (2016)
David R. Cok, Aaron Stump, Tjark Weber
The 2013 Evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55 (1) (2015)
Ryan McCleeary, Martin Brain, Aaron Stump
A lazy approach to adaptive exact real arithmetic using floating-point operations. ACM Commun. Comput. Algebra 49 (3) (2015)
Aaron Stump
The recursive polarized dual calculus. PLPV (2014)
Aaron Stump, Geoff Sutcliffe, Cesare Tinelli
StarExec: A Cross-Community Infrastructure for Logic Solving. IJCAR (2014)
Peng Fu, Aaron Stump
Self Types for Dependently Typed Lambda Encodings. RTA-TLCA (2014)
Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli
SMT proof checking using a logical framework. Formal Methods Syst. Des. 42 (1) (2013)
Harley Eades III, Aaron Stump
Hereditary Substitution for the λΔ-Calculus. COS (2013)
Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump
6 Years of SMT-COMP. J. Autom. Reason. 50 (3) (2013)
Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn
Equational reasoning about programs with general recursion and call-by-value semantics. PLPV (2012)
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump
The 2nd Verified Software Competition: Experience Report. COMPARE (2012)
Jacques Carette, Aaron Stump
Towards typing for small-step direct reflection. PEPM (2012)
Aaron Stump, Geoff Sutcliffe, Cesare Tinelli
Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. COMPARE (2012)
Adam M. Procter, William L. Harrison, Aaron Stump
The Design of a Practical Proof Checker for a Lazy Functional Language. Trends in Functional Programming (2012)
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems MSFP (2012)
Aaron Stump, Hans Zantema, Garrin Kimmell, Roba El Haj Omar
A Rewriting View of Simple Typing Log. Methods Comput. Sci. 9 (1) (2012)
Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy
versat: A Verified Modern SAT Solver. VMCAI (2012)
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang
LFSC for SMT Proofs: Work in Progress. PxTP (2012)
Aaron Stump, Garrin Kimmell, Roba El Haj Omar
Type Preservation as a Confluence Problem. RTA (2011)
Tim Sheard, Aaron Stump, Stephanie Weirich
Language-based verification will change the world. FoSER (2010)
Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference (2010)
Aaron Stump, Evan Austin
Resource typing in Guru. PLPV (2010)
Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
Termination Casts: A Flexible Approach to Termination with General Recursion PAR (2010)
Vilhelm Sjöberg, Aaron Stump
Equality, Quasi-Implicit Products, and Large Eliminations ITRS (2010)
Robert Brummayer, Duckki Oe, Aaron Stump
Exploring Predictability of SAT/SMT Solvers. EMSQMS@IJCAR (2010)
Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
Termination Casts: A Flexible Approach to Termination with General Recursion. PAR@ITP (2010)
Aaron Stump, Evan Austin
Resource typing in guru: (abstract only). ACM SIGPLAN Notices 44 (11) (2009)
Edwin M. Westbrook, Aaron Stump, Evan Austin
The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings. LFMTP (2009)
Aaron Stump
Directly reflective meta-programming. High. Order Symb. Comput. 22 (2) (2009)
Aaron Stump
Proof Checking Technology for Satisfiability Modulo Theories. Electron. Notes Theor. Comput. Sci. 228 (2009)
Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson
Verified programming in Guru. PLPV (2009)
Michael Zeller, Aaron Stump, Morgan Deters
Signature Compilation for the Edinburgh Logical Framework. Electron. Notes Theor. Comput. Sci. 196 (2008)
Clark W. Barrett, Morgan Deters, Albert Oliveras, Aaron Stump
Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). Int. J. Artif. Intell. Tools 17 (4) (2008)
Aaron Stump
Imperative LF Meta-Programming. Electron. Notes Theor. Comput. Sci. 199 (2008)
Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods Syst. Des. 31 (3) (2007)
Aaron Stump, Hongwei Xi
Preface. Electron. Notes Theor. Comput. Sci. 174 (7) (2007)
Aaron Stump
Lightweight Verification with Dependent Types. VERIFY (2007)
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, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump
Roadmap for enhanced languages and methods to aid verification. GPCE (2006)
Ian Wehrman, Aaron Stump, Edwin M. Westbrook
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker. RTA (2006)
Ian Wehrman, Aaron Stump
Mining Propositional Simplification Proofs for Small Validating Clauses. Electron. Notes Theor. Comput. Sci. 144 (2) (2006)
Aaron Stump, Bernd Löchner
Knuth-Bendix completion of theories of commuting group endomorphisms. Inf. Process. Lett. 98 (5) (2006)
Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
SMT-COMP: Satisfiability Modulo Theories Competition. CAV (2005)
Edwin M. Westbrook, Aaron Stump, Ian Wehrman
A language-based approach to functionally correct imperative programming. ICFP (2005)
Aaron Stump, Li-Yang Tan
The Algebra of Equality Proofs. RTA (2005)
Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. 35 (4) (2005)
Aaron Stump, Carsten Schürmann
Logical Semantics for the Rewriting Calculus. Electron. Notes Theor. Comput. Sci. 125 (2) (2005)
Robert Klapper, Aaron Stump
Validated Proof-Producing Decision Procedures. Electron. Notes Theor. Comput. Sci. 125 (3) (2005)
Aaron Stump
Programming with Proofs: Language-Based Approaches to Totally Correct Software. VSTTE (2005)
Aaron Stump, Ryan Besand, James C. Brodman, Jonathan Hseu, Bill Kinnersley
From Rogue to MicroRogue. WRLA (2004)
Dinghao Wu, Andrew W. Appel, Aaron Stump
Foundational proof checkers with small witnesses. PPDP (2003)
Aaron Stump
Subset Types and Partial Functions. CADE (2003)
Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga
A Trustworthy Proof Checker. J. Autom. Reason. 31 (3-4) (2003)
Clark W. Barrett, David L. Dill, Aaron Stump
A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS (2002)
Aaron Stump, Clark W. Barrett, David L. Dill
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. Electron. Notes Theor. Comput. Sci. 70 (2) (2002)
Clark W. Barrett, David L. Dill, Aaron Stump
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV (2002)
Aaron Stump, Clark W. Barrett, David L. Dill
CVC: A Cooperating Validity Checker. CAV (2002)
Aaron Stump, David L. Dill
Faster Proof Checking in the Edinburgh Logical Framework. CADE (2002)
Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt
A Decision Procedure for an Extensional Theory of Arrays. LICS (2001)
Clark W. Barrett, David L. Dill, Aaron Stump
A Framework for Cooperating Decision Procedures. CADE (2000)