Aaron Stump - RankMe

94 papers A* 4A 5B 4C 2Journal 32Unranked 41

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