David Van Horn

91 papers A* 6A 12B 3C 2Journal 59Unranked 6

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Webs and Flow-Directed Well-Typedness Preserving Program Transformations. Proc. ACM Program. Lang. Benjamin Quiring, David Van Horn, John H. Reppy, Olin Shivers
2024	J	`jnl`	Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis. Proc. ACM Program. Lang. Benjamin Quiring, David Van Horn
2023	J	`jnl`	A formal model of Checked C. J. Comput. Secur. Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2023	J	`jnl`	Absynthe: Abstract Interpretation-Guided Synthesis. CoRR Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
2023	J	`jnl`	Absynthe: Abstract Interpretation-Guided Synthesis. Proc. ACM Program. Lang. Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
2022	A	`conf`	A Formal Model of Checked C. CSF Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2022	J	`jnl`	A Formal Model of Checked C. CoRR Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2021	J	`jnl`	Corpse reviver: sound and efficient gradual typing via contract verification. Proc. ACM Program. Lang. Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
2021	J	`jnl`	RbSyn: Type- and Effect-Guided Program Synthesis. CoRR Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
2021	A*	`conf`	RbSyn: type- and effect-guided program synthesis. PLDI Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
2020	J	`jnl`	Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification. CoRR Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
2019	J	`jnl`	Constructive Galois Connections. J. Funct. Program. David Darais, David Van Horn
2019	A*	`conf`	Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs. PLDI Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
2019	—	`ed.`	Trends in Functional Programming - 17th International Conference, TFP 2016, College Park, MD, USA, June 8-10, 2016, Revised Selected Papers TFP David Van Horn, John Hughes
2019	J	`jnl`	Type-Level Computations for Ruby Libraries. CoRR Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
2019	A*	`conf`	Type-level computations for Ruby libraries. PLDI Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
2018	J	`jnl`	Constructive Galois Connections. CoRR David Darais, David Van Horn
2018	J	`jnl`	Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). CoRR Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton
2018	J	`jnl`	Gradual Liquid Type Inference. CoRR Niki Vazou, Éric Tanter, David Van Horn
2018	J	`jnl`	Gradual liquid type inference. Proc. ACM Program. Lang. Niki Vazou, Éric Tanter, David Van Horn
2018	J	`jnl`	Size-Change Termination as a Contract. CoRR Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
2018	J	`jnl`	Soft contract verification for higher-order stateful programs. Proc. ACM Program. Lang. Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
2018	—	`conf`	Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). Haskell@ICFP Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton
2017	J	`jnl`	Abstracting Definitional Interpreters. CoRR David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn
2017	J	`jnl`	Abstracting definitional interpreters (functional pearl). Proc. ACM Program. Lang. David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn
2017	J	`jnl`	Higher order symbolic execution for contract verification and refutation. J. Funct. Program. Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
2017	J	`jnl`	Soft Contract Verification for Higher-Order Stateful Programs. CoRR Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
2016	J	`jnl`	A Vision for Online Verification-Validation. CoRR Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn
2016	B	`conf`	A vision for online verification-validation. GPCE Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn
2016	A	`conf`	Constructive Galois connections: taming the Galois connection framework for mechanized metatheory. ICFP David Darais, David Van Horn
2016	A*	`conf`	Pushdown control-flow analysis for free. POPL Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn
2015	J	`jnl`	Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory. CoRR David Darais, David Van Horn
2015	A	`conf`	Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. OOPSLA David Darais, Matthew Might, David Van Horn
2015	J	`jnl`	Higher-order symbolic execution for contract verification and refutation. CoRR Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
2015	J	`jnl`	Incremental Computation with Names. CoRR Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael Hicks, David Van Horn
2015	A	`conf`	Incremental computation with names. OOPSLA Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, David Van Horn
2015	J	`jnl`	Mechanically Verified Calculational Abstract Interpretation. CoRR David Darais, David Van Horn
2015	J	`jnl`	Pushdown Control-Flow Analysis for Free. CoRR Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn
2015	A*	`conf`	Relatively complete counterexamples for higher-order programs. PLDI Phuc C. Nguyen, David Van Horn
2015	A	`conf`	Running Probabilistic Programs Backwards. ESOP Neil Toronto, Jay McCarthy, David Van Horn
2015	J	`jnl`	The use of analytics in the design of sociotechnical products. Artif. Intell. Eng. Des. Anal. Manuf. David Van Horn, Kemper Lewis
2014	C	`conf`	Abstracting abstract control. DLS Dionna Amalie Glaze, David Van Horn
2014	J	`jnl`	Galois Transformers and Modular Abstract Interpreters. CoRR David Darais, Matthew Might, David Van Horn
2014	C	`conf`	Pruning, Pushdown Exception-Flow Analysis. SCAM Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn
2014	J	`jnl`	Pruning, Pushdown Exception-Flow Analysis. CoRR Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn
2014	J	`jnl`	Pushdown flow analysis with abstract garbage collection. CoRR Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
2014	J	`jnl`	Pushdown flow analysis with abstract garbage collection. J. Funct. Program. Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
2014	J	`jnl`	Relatively Complete Counterexamples for Higher-Order Programs. CoRR Phuc C. Nguyen, David Van Horn
2014	J	`jnl`	Running Probabilistic Programs Backwards. CoRR Neil Toronto, Jay McCarthy, David Van Horn
2014	A	`conf`	Soft contract verification. ICFP Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
2013	J	`jnl`	AnaDroid: Malware Analysis of Android with User-supplied Predicates. CoRR Shuying Liang, Matthew Might, David Van Horn
2013	—	`conf`	AnaDroid: Malware Analysis of Android with User-supplied Predicates. TAPAS@SAS Shuying Liang, Matthew Might, David Van Horn
2013	J	`jnl`	Concrete Semantics for Pushdown Analysis: The Essence of Summarization CoRR Dionna Amalie Glaze, David Van Horn
2013	J	`jnl`	Deciding $k$CFA is complete for EXPTIME. CoRR David Van Horn, Harry G. Mairson
2013	J	`jnl`	Flow analysis, linearity, and PTIME. CoRR David Van Horn, Harry G. Mairson
2013	—	`conf`	From Principles to Practice with Class in the First Year. TFPIE Sam Tobin-Hochstadt, David Van Horn
2013	A	`conf`	Optimizing abstract abstract machines. ICFP Dionna Amalie Glaze, Nicholas Labich, Matthew Might, David Van Horn
2013	—	`ed.`	Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013 PLPV Matthew Might, David Van Horn, Andreas Abel, Tim Sheard
2013	J	`jnl`	Pushdown Exception-Flow Analysis of Object-Oriented Programs CoRR Shuying Liang, Matthew Might, Thomas Gilray, David Van Horn
2013	—	`book`	Realm of Racket - Learn to Program, One Game at a Time! Matthias Felleisen, David Van Horn, Conrad Barski
2013	J	`jnl`	Resolving and Exploiting the $k$-CFA Paradox. CoRR Matthew Might, Yannis Smaragdakis, David Van Horn
2013	J	`jnl`	Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. CoRR Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, David Van Horn
2013	—	`conf`	Sound and precise malware analysis for android via pushdown reachability and entry-point saturation. SPSM@CCS Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, David Van Horn
2013	J	`jnl`	Static Contract Checking for Scripting Languages. CoRR Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
2013	J	`jnl`	The Complexity of Flow Analysis in Higher-Order Languages. CoRR David Van Horn
2012	A	`conf`	Higher-order symbolic execution via contracts. OOPSLA Sam Tobin-Hochstadt, David Van Horn
2012	J	`jnl`	Introspective Pushdown Analysis of Higher-Order Programs CoRR Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
2012	A	`conf`	Introspective pushdown analysis of higher-order programs. ICFP Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
2012	J	`jnl`	Optimizing Abstract Abstract Machines CoRR Dionna Amalie Glaze, Matthew Might, David Van Horn
2012	J	`jnl`	Systematic abstraction of abstract machines. J. Funct. Program. David Van Horn, Matthew Might
2011	B	`conf`	A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. SAS Matthew Might, David Van Horn
2011	J	`jnl`	A family of abstract interpretations for static analysis of concurrent higher-order programs CoRR Matthew Might, David Van Horn
2011	J	`jnl`	Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis CoRR David Van Horn, Matthew Might
2011	J	`jnl`	Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM David Van Horn, Matthew Might
2011	J	`jnl`	An Analytic Framework for JavaScript CoRR David Van Horn, Matthew Might
2011	J	`jnl`	Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). NII Shonan Meet. Rep. Naoki Kobayashi, Luke Ong, David Van Horn
2011	J	`jnl`	Modular Analysis via Specifications as Values CoRR Sam Tobin-Hochstadt, David Van Horn
2011	J	`jnl`	Semantic Solutions to Program Analysis Problems CoRR Sam Tobin-Hochstadt, David Van Horn
2011	J	`jnl`	Systematic Abstraction of Abstract Machines CoRR David Van Horn, Matthew Might
2010	J	`jnl`	Abstracting Abstract Machines CoRR David Van Horn, Matthew Might
2010	A	`conf`	Abstracting abstract machines. ICFP David Van Horn, Matthew Might
2010	J	`jnl`	Evaluating Call-By-Need on the Control Stack CoRR Stephen Chang, David Van Horn, Matthias Felleisen
2010	—	`conf`	Evaluating Call-by-Need on the Control Stack. Trends in Functional Programming Stephen Chang, David Van Horn, Matthias Felleisen
2010	J	`jnl`	Pushdown Control-Flow Analysis of Higher-Order Programs CoRR Christopher Earl, Matthew Might, David Van Horn
2010	A*	`conf`	Resolving and exploiting the PLDI Matthew Might, Yannis Smaragdakis, David Van Horn
2010	J	`jnl`	Stack-Summarizing Control-Flow Analysis of Higher-Order Programs CoRR Christopher Earl, Matthew Might, David Van Horn
2008	A	`conf`	Deciding ICFP David Van Horn, Harry G. Mairson
2008	B	`conf`	Flow Analysis, Linearity, and PTIME. SAS David Van Horn, Harry G. Mairson
2008	J	`jnl`	Types and trace effects of higher order programs. J. Funct. Program. Christian Skalka, Scott F. Smith, David Van Horn
2007	A	`conf`	Relating complexity and precision in control flow analysis. ICFP David Van Horn, Harry G. Mairson
2005	—	`conf`	A Type and Effect System for Flexible Abstract Interpretation of Java: (Extended Abstract). AIOOL@VMCAI Christian Skalka, Scott F. Smith, David Van Horn