Aaron Stump

According to our database1, Aaron Stump authored at least 76 papers between 2000 and 2021.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2021
Relational Type Theory (All Proofs).
CoRR, 2021

2020
Strong functional pearl: Harper's regular-expression matcher in Cedille.
Proc. ACM Program. Lang., 2020

Efficient lambda encodings for Mendler-style coinductive types in Cedille.
Proceedings of the Proceedings Eighth Workshop on Mathematically Structured Functional Programming, 2020

Monotone recursive types and recursive data representations in Cedille.
CoRR, 2020

2019
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille.
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.
CoRR, 2019

Quotients by Idempotent Functions in Cedille.
Proceedings of the Trends in Functional Programming - 20th International Symposium, 2019

2018
Generic zero-cost reuse for dependent types.
Proc. ACM Program. Lang., 2018

Course-of-Value Induction in Cedille.
CoRR, 2018

Syntax and Typing for Cedille Core.
CoRR, 2018

Syntax and Semantics of Cedille.
CoRR, 2018

Zero-Cost Coercions for Program and Proof Reuse.
CoRR, 2018

From realizability to induction via dependent intersection.
Ann. Pure Appl. Log., 2018

Efficient Mendler-Style Lambda-Encodings in Cedille.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Spine-local Type Inference.
Proceedings of the 30th Symposium on Implementation and Application of Functional Languages, 2018

Generic derivation of induction for impredicative encodings in Cedille.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
The calculus of dependent lambda eliminations.
J. Funct. Program., 2017

2016
Efficiency of lambda-encodings in total type theory.
J. Funct. Program., 2016

Dualized Simple Type Theory.
Log. Methods Comput. Sci., 2016

Project Report: Dependently Typed Programming with Lambda Encodings in Cedille.
Proceedings of the Trends in Functional Programming - 17th International Conference, 2016

2015
The 2013 Evaluation of SMT-COMP and SMT-LIB.
J. Autom. Reason., 2015

A lazy approach to adaptive exact real arithmetic using floating-point operations.
ACM Commun. Comput. Algebra, 2015

2014
Self Types for Dependently Typed Lambda Encodings.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

The recursive polarized dual calculus.
Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2014

StarExec: A Cross-Community Infrastructure for Logic Solving.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
6 Years of SMT-COMP.
J. Autom. Reason., 2013

SMT proof checking using a logical framework.
Formal Methods Syst. Des., 2013

Hereditary Substitution for the λΔ-Calculus.
Proceedings of the Proceedings First Workshop on Control Operators and their Semantics, 2013

2012
A Rewriting View of Simple Typing
Log. Methods Comput. Sci., 2012

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Proceedings of the Proceedings Fourth Workshop on Mathematically Structured Functional Programming, 2012

versat: A Verified Modern SAT Solver.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

The Design of a Practical Proof Checker for a Lazy Functional Language.
Proceedings of the Trends in Functional Programming - 13th International Symposium, 2012

Equational reasoning about programs with general recursion and call-by-value semantics.
Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

Towards typing for small-step direct reflection.
Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, 2012

Introducing StarExec: a Cross-Community Infrastructure for Logic Solving.
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

The 2nd Verified Software Competition: Experience Report.
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

2011
Type Preservation as a Confluence Problem.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

2010
Equality, Quasi-Implicit Products, and Large Eliminations
Proceedings of the Proceedings Fifth Workshop on Intersection Types and Related Systems, 2010

Termination Casts: A Flexible Approach to Termination with General Recursion
Proceedings of the Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010

Language-based verification will change the world.
Proceedings of the Workshop on Future of Software Engineering Research, 2010

Resource typing in Guru.
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).
Proceedings of the Hardware and Software: Verification and Testing, 2010

Exploring Predictability of SAT/SMT Solvers.
Proceedings of the Workshop on Evaluation Methods for Solvers, 2010

2009
Resource typing in guru: (abstract only).
ACM SIGPLAN Notices, 2009

Directly reflective meta-programming.
High. Order Symb. Comput., 2009

Proof Checking Technology for Satisfiability Modulo Theories.
Electron. Notes Theor. Comput. Sci., 2009

Verified programming in Guru.
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.
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).
Int. J. Artif. Intell. Tools, 2008

Signature Compilation for the Edinburgh Logical Framework.
Electron. Notes Theor. Comput. Sci., 2008

Imperative LF Meta-Programming.
Electron. Notes Theor. Comput. Sci., 2008

2007
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006).
Formal Methods Syst. Des., 2007

Preface.
Electron. Notes Theor. Comput. Sci., 2007

Lightweight Verification with Dependent Types.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006
Knuth-Bendix completion of theories of commuting group endomorphisms.
Inf. Process. Lett., 2006

Mining Propositional Simplification Proofs for Small Validating Clauses.
Electron. Notes Theor. Comput. Sci., 2006

Slothrop: Knuth-Bendix Completion with a Modern Termination Checker.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Roadmap for enhanced languages and methods to aid verification.
Proceedings of the Generative Programming and Component Engineering, 2006

2005
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005).
J. Autom. Reason., 2005

Logical Semantics for the Rewriting Calculus.
Electron. Notes Theor. Comput. Sci., 2005

Validated Proof-Producing Decision Procedures.
Electron. Notes Theor. Comput. Sci., 2005

Programming with Proofs: Language-Based Approaches to Totally Correct Software.
Proceedings of the Verified Software: Theories, 2005

The Algebra of Equality Proofs.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

A language-based approach to functionally correct imperative programming.
Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

SMT-COMP: Satisfiability Modulo Theories Competition.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
From Rogue to MicroRogue.
Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 2004

2003
A Trustworthy Proof Checker.
J. Autom. Reason., 2003

Foundational proof checkers with small witnesses.
Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

Subset Types and Partial Functions.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.
Electron. Notes Theor. Comput. Sci., 2002

A Generalization of Shostak's Method for Combining Decision Procedures.
Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

CVC: A Cooperating Validity Checker.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Faster Proof Checking in the Edinburgh Logical Framework.
Proceedings of the Automated Deduction, 2002

2001
A Decision Procedure for an Extensional Theory of Arrays.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000
A Framework for Cooperating Decision Procedures.
Proceedings of the Automated Deduction, 2000


  Loading...