AS
Aaron Stump
cs.PLcs.LO
On Valency
published · living versionsW_zm8usghj·v1 · currentpublished
Preprints & journals
20 papers in the corpus · 2010–2026Natural Deduction Derivations as Directed Acyclic Proof Graphs2610.27196v1 · Jonathan Chan, Aaron Stump2026 · 0 citationsarXivon Valency
Simulating Large Eliminations in Cedille2112.07817v1 · Christopher Jenkins, Andrew Marmaduke, Aaron Stump2021 · 1 citationarXiv
Relational Type Theory (All Proofs)2101.09655v1 · Aaron Stump, Benjamin Delaware, Christopher Jenkins2021 · 0 citationsarXiv
Efficient lambda encodings for Mendler-style coinductive types in Cedille2005.00199v1 · Christopher Jenkins, Aaron Stump, Larry Diehl2020 · 0 citationsEPTCS 317, 2020, pp. 72-97
Monotone recursive types and recursive data representations in Cedille2001.02828v2 · Christopher Jenkins, Aaron Stump2020 · 2 citationsMath. Struct. Comp. Sci. 31 (2021) 682-745
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille1910.10851v1 · Aaron Stump2019 · 0 citationsEPTCS 307, 2019, pp. 55-67
Elaborating Inductive Definitions and Course-of-Values Induction in Cedille1903.08233v3 · Christopher Jenkins, Colin McDonald, Aaron Stump2019 · 0 citationsarXiv
Course-of-Value Induction in Cedille1811.11961v2 · Denis Firsov, Larry Diehl, Christopher Jenkins et al.2018 · 2 citationsarXiv
Syntax and Typing for Cedille Core1811.01318v1 · Aaron Stump2018 · 2 citationsarXiv
Syntax and Semantics of Cedille1806.04709v3 · Aaron Stump, Christopher Jenkins2018 · 4 citationsarXiv
Spine-local Type Inference1805.10383v1 · Christopher Jenkins, Aaron Stump2018 · 5 citationsarXiv
Generic Zero-Cost Reuse for Dependent Types1803.08150v3 · Larry Diehl, Denis Firsov, Aaron Stump2018 · 10 citationsarXiv
Efficient Mendler-Style Lambda-Encodings in Cedille1803.02473v1 · Denis Firsov, Richard Blair, Aaron Stump2018 · 8 citationsarXiv
Zero-Cost Coercions for Program and Proof Reuse1802.00787v1 · Larry Diehl, Aaron Stump2018 · 0 citationsarXiv
Dualized Simple Type Theory1605.01083v2 · Harley Eades III, Aaron Stump, Ryan McCleeary2016 · 2 citationsLogical Methods in Computer Science, Volume 12, Issue 3 (April 27, 2017) lmcs:2005
Hereditary Substitution for the \lambda\Delta-Calculus1309.1256v1 · Harley Eades, Aaron Stump2013 · 1 citationEPTCS 127, 2013, pp. 45-65
A Rewriting View of Simple Typing1211.0865v2 · Aaron Stump, Garrin Kimmell, Hans Zantema (TU Eindhoven) et al.2012 · 2 citationsLogical Methods in Computer Science, Volume 9, Issue 1 (February 27, 2013) lmcs:936
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems1202.2923v1 · Vilhelm Sjoberg, Chris Casinghino, Ki Yung Ahn et al.2012 · 17 citationsEPTCS 76, 2012, pp. 112-162
Equality, Quasi-Implicit Products, and Large Eliminations1101.4430v1 · Vilhelm Sjoberg, Aaron Stump2011 · 4 citationsEPTCS 45, 2011, pp. 90-100
Termination Casts: A Flexible Approach to Termination with General Recursion1012.4900v1 · Aaron Stump, Vilhelm Sjoberg, Stephanie Weirich2010 · 4 citationsEPTCS 43, 2010, pp. 76-93
Career total: 179 works. 20 are in this corpus.
Profile built from the corpus for this byline.
Author records are still filling in while the Hub is in alpha. If this is your page, you'll be able to claim it soon. Spot a mistake? Tell us.