Aaron Stump

According to our database, Aaron Stump authored at least 84 papers between 2000 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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., January, 2023

Impredicative Encodings of Inductive-Inductive Data in Cedille.

Andrew Marmaduke, Larry Diehl, Aaron Stump

Proceedings of the Trends in Functional Programming - 24th International Symposium, 2023

2021

Monotone recursive types and recursive data representations in Cedille.

Christopher Jenkins, Aaron Stump

Math. Struct. Comput. Sci., 2021

Simulating Large Eliminations in Cedille.

Christopher Jenkins, Andrew Marmaduke, Aaron Stump

CoRR, 2021

Relational Type Theory (All Proofs).

Aaron Stump, Benjamin Delaware, Christopher Jenkins

CoRR, 2021

Simulating Large Eliminations in Cedille.

Christa Jenkins, Andrew Marmaduke, Aaron Stump

Proceedings of the 27th International Conference on Types for Proofs and Programs, 2021

2020

Strong functional pearl: Harper's regular-expression matcher in Cedille.

Aaron Stump, Christopher Jenkins, Stephan Spahn, Colin McDonald

Proc. ACM Program. Lang., 2020

Efficient lambda encodings for Mendler-style coinductive types in Cedille.

Christopher Jenkins, Aaron Stump, Larry Diehl

Proceedings of the Proceedings Eighth Workshop on Mathematically Structured Functional Programming, 2020

Zero-Cost Constructor Subtyping.

Andrew Marmaduke, Christopher Jenkins, Aaron Stump

Proceedings of the IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages, 2020

2019

A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille.

Aaron Stump

Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2019

Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille.

Christopher Jenkins, Colin McDonald, Aaron Stump

CoRR, 2019

Quotients by Idempotent Functions in Cedille.

Andrew Marmaduke, Christopher Jenkins, Aaron Stump

Proceedings of the Trends in Functional Programming - 20th International Symposium, 2019

2018

Generic zero-cost reuse for dependent types.

Larry Diehl, Denis Firsov, Aaron Stump

Proc. ACM Program. Lang., 2018

Course-of-Value Induction in Cedille.

Denis Firsov, Larry Diehl, Christopher Jenkins, Aaron Stump

CoRR, 2018

Syntax and Typing for Cedille Core.

Aaron Stump

CoRR, 2018

Syntax and Semantics of Cedille.

Aaron Stump

CoRR, 2018

Zero-Cost Coercions for Program and Proof Reuse.

Larry Diehl, Aaron Stump

CoRR, 2018

From realizability to induction via dependent intersection.

Aaron Stump

Ann. Pure Appl. Log., 2018

Efficient Mendler-Style Lambda-Encodings in Cedille.

Denis Firsov, Richard Blair, Aaron Stump

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Spine-local Type Inference.

Christopher Jenkins, Aaron Stump

Proceedings of the 30th Symposium on Implementation and Application of Functional Languages, 2018

Generic derivation of induction for impredicative encodings in Cedille.

Denis Firsov, Aaron Stump

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

The calculus of dependent lambda eliminations.

Aaron Stump

J. Funct. Program., 2017

2016

Efficiency of lambda-encodings in total type theory.

Aaron Stump, Peng Fu

J. Funct. Program., 2016

Dualized Simple Type Theory.

Harley Eades III, Aaron Stump, Ryan McCleeary

Log. Methods Comput. Sci., 2016

Project Report: Dependently Typed Programming with Lambda Encodings in Cedille.

Ananda Guneratne, Chad Reynolds, Aaron Stump

Proceedings of the Trends in Functional Programming - 17th International Conference, 2016

Verified Functional Programming in Agda

Aaron Stump

ACM Books 9, ACM, ISBN: 978-1-970001-27-3, 2016

2015

The 2013 Evaluation of SMT-COMP and SMT-LIB.

David R. Cok, Aaron Stump, Tjark Weber

J. Autom. Reason., 2015

A lazy approach to adaptive exact real arithmetic using floating-point operations.

Ryan McCleeary, Martin Brain, Aaron Stump

ACM Commun. Comput. Algebra, 2015

2014

Self Types for Dependently Typed Lambda Encodings.

Peng Fu, Aaron Stump

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

The recursive polarized dual calculus.

Aaron Stump

Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2014

StarExec: A Cross-Community Infrastructure for Logic Solving.

Aaron Stump, Geoff Sutcliffe, Cesare Tinelli

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

6 Years of SMT-COMP.

Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump

J. Autom. Reason., 2013

SMT proof checking using a logical framework.

Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli

Formal Methods Syst. Des., 2013

Hereditary Substitution for the λΔ-Calculus.

Harley Eades III, Aaron Stump

Proceedings of the Proceedings First Workshop on Control Operators and their Semantics, 2013

2012

A Rewriting View of Simple Typing

Aaron Stump, Hans Zantema, Garrin Kimmell, Roba El Haj Omar

Log. Methods Comput. Sci., 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, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich

Proceedings of the Proceedings Fourth Workshop on Mathematically Structured Functional Programming, 2012

versat: A Verified Modern SAT Solver.

Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

The Design of a Practical Proof Checker for a Lazy Functional Language.

Adam M. Procter, William L. Harrison, Aaron Stump

Proceedings of the Trends in Functional Programming - 13th International Symposium, 2012

LFSC for SMT Proofs: Work in Progress.

Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

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 Sjöberg, Nathan Collins, Ki Yung Ahn

Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

Towards typing for small-step direct reflection.

Jacques Carette, Aaron Stump

Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, 2012

Introducing StarExec: a Cross-Community Infrastructure for Logic Solving.

Aaron Stump, Geoff Sutcliffe, Cesare Tinelli

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

The 2nd Verified Software Competition: Experience Report.

Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

2011

Type Preservation as a Confluence Problem.

Aaron Stump, Garrin Kimmell, Roba El Haj Omar

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

2010

Equality, Quasi-Implicit Products, and Large Eliminations

Vilhelm Sjöberg, Aaron Stump

Proceedings of the Proceedings Fifth Workshop on Intersection Types and Related Systems, 2010

Termination Casts: A Flexible Approach to Termination with General Recursion

Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich

Proceedings of the Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010

Language-based verification will change the world.

Tim Sheard, Aaron Stump, Stephanie Weirich

Proceedings of the Workshop on Future of Software Engineering Research, 2010

Resource typing in Guru.

Aaron Stump, Evan Austin

Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, 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

Proceedings of the Hardware and Software: Verification and Testing, 2010

Exploring Predictability of SAT/SMT Solvers.

Robert Brummayer, Duckki Oe, Aaron Stump

Proceedings of the Workshop on Evaluation Methods for Solvers, 2010

2009

Resource typing in guru: (abstract only).

Aaron Stump, Evan Austin

ACM SIGPLAN Notices, 2009

Directly reflective meta-programming.

Aaron Stump

High. Order Symb. Comput., 2009

Verified programming in Guru.

Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson

Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, 2009

The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings.

Edwin M. Westbrook, Aaron Stump, Evan Austin

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009

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

Proof Checking Technology for Satisfiability Modulo Theories.

Aaron Stump

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

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

Signature Compilation for the Edinburgh Logical Framework.

Michael Zeller, Aaron Stump, Morgan Deters

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

Lightweight Verification with Dependent Types.

Aaron Stump

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006

Knuth-Bendix completion of theories of commuting group endomorphisms.

Aaron Stump, Bernd Löchner

Inf. Process. Lett., 2006

Preface.

Aaron Stump, Hongwei Xi

Proceedings of the Programming Languages meets Program Verification, 2006

Slothrop: Knuth-Bendix Completion with a Modern Termination Checker.

Ian Wehrman, Aaron Stump, Edwin M. Westbrook

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

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, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump

Proceedings of the Generative Programming and Component Engineering, 2006

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

Mining Propositional Simplification Proofs for Small Validating Clauses.

Ian Wehrman, Aaron Stump

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Programming with Proofs: Language-Based Approaches to Totally Correct Software.

Aaron Stump

Proceedings of the Verified Software: Theories, 2005

The Algebra of Equality Proofs.

Aaron Stump, Li-Yang Tan

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

A language-based approach to functionally correct imperative programming.

Edwin M. Westbrook, Aaron Stump, Ian Wehrman

Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

SMT-COMP: Satisfiability Modulo Theories Competition.

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Logical Semantics for the Rewriting Calculus.

Aaron Stump, Carsten Schürmann

Proceedings of the 5th International Workshop on Strategies in Automated Deduction, 2004

From Rogue to MicroRogue.

Aaron Stump, Ryan Besand, James C. Brodman, Jonathan Hseu, Bill Kinnersley

Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 2004

Imperative LF Meta-Programming.

Aaron Stump

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Validated Proof-Producing Decision Procedures.

Robert Klapper, Aaron Stump

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

2003

A Trustworthy Proof Checker.

Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga

J. Autom. Reason., 2003

Foundational proof checkers with small witnesses.

Dinghao Wu, Andrew W. Appel, Aaron Stump

Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

Subset Types and Partial Functions.

Aaron Stump

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Checking validities and proofs with CVC and flea.

Aaron Stump

PhD thesis, 2002

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.

Aaron Stump, Clark W. Barrett, David L. Dill

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

A Generalization of Shostak's Method for Combining Decision Procedures.

Clark W. Barrett, David L. Dill, Aaron Stump

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

CVC: A Cooperating Validity Checker.

Aaron Stump, Clark W. Barrett, David L. Dill

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.

Clark W. Barrett, David L. Dill, Aaron Stump

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Faster Proof Checking in the Edinburgh Logical Framework.

Aaron Stump, David L. Dill

Proceedings of the Automated Deduction, 2002

2001

A Decision Procedure for an Extensional Theory of Arrays.

Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

A Framework for Cooperating Decision Procedures.

Clark W. Barrett, David L. Dill, Aaron Stump

Proceedings of the Automated Deduction, 2000