David Van Horn

According to our database, David Van Horn authored at least 61 papers between 2005 and 2024.

Collaborative distances:

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

2024

Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis.

Benjamin Quiring, David Van Horn

Proc. ACM Program. Lang., 2024

2023

Absynthe: Abstract Interpretation-Guided Synthesis.

Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn

Proc. ACM Program. Lang., 2023

A formal model of Checked C.

Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks

J. Comput. Secur., 2023

2021

Corpse reviver: sound and efficient gradual typing via contract verification.

Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn

Proc. ACM Program. Lang., 2021

RbSyn: type- and effect-guided program synthesis.

Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2019

Constructive Galois Connections.

David Darais, David Van Horn

J. Funct. Program., 2019

Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs.

Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Type-level computations for Ruby libraries.

Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018

Gradual liquid type inference.

Niki Vazou, Éric Tanter, David Van Horn

Proc. ACM Program. Lang., 2018

Soft contract verification for higher-order stateful programs.

Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

Proc. ACM Program. Lang., 2018

Size-Change Termination as a Contract.

Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

CoRR, 2018

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell).

Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton

CoRR, 2018

Theorem proving for all: equational reasoning in liquid Haskell (functional pearl).

Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton

Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, 2018

2017

Abstracting definitional interpreters (functional pearl).

David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn

Proc. ACM Program. Lang., 2017

Higher order symbolic execution for contract verification and refutation.

Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn

J. Funct. Program., 2017

Abstracting Definitional Interpreters.

David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn

CoRR, 2017

2016

Pushdown control-flow analysis for free.

Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory.

David Darais, David Van Horn

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

A vision for online verification-validation.

Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn

Proceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, 2016

2015

Mechanically Verified Calculational Abstract Interpretation.

David Darais, David Van Horn

CoRR, 2015

The use of analytics in the design of sociotechnical products.

David Van Horn, Kemper Lewis

Artif. Intell. Eng. Des. Anal. Manuf., 2015

Relatively complete counterexamples for higher-order programs.

Phuc C. Nguyen, David Van Horn

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Incremental computation with names.

Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, David Van Horn

Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Galois transformers and modular abstract interpreters: reusable metatheory for program analysis.

David Darais, Matthew Might, David Van Horn

Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Running Probabilistic Programs Backwards.

Neil Toronto, Jay McCarthy, David Van Horn

Proceedings of the Programming Languages and Systems, 2015

2014

Pushdown flow analysis with abstract garbage collection.

Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn

J. Funct. Program., 2014

Galois Transformers and Modular Abstract Interpreters.

David Darais, Matthew Might, David Van Horn

CoRR, 2014

Pruning, Pushdown Exception-Flow Analysis.

Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn

Proceedings of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation, 2014

Soft contract verification.

Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

Abstracting abstract control.

Dionna Amalie Glaze, David Van Horn

Proceedings of the DLS'14, 2014

2013

AnaDroid: Malware Analysis of Android with User-supplied Predicates.

Shuying Liang, Matthew Might, David Van Horn

Proceedings of the Fourth Workshop on Tools for Automatic Program Analysis, 2013

Concrete Semantics for Pushdown Analysis: The Essence of Summarization

Dionna Amalie Glaze, David Van Horn

CoRR, 2013

Pushdown Exception-Flow Analysis of Object-Oriented Programs

Shuying Liang, Matthew Might, Thomas Gilray, David Van Horn

CoRR, 2013

From Principles to Practice with Class in the First Year.

Sam Tobin-Hochstadt, David Van Horn

Proceedings of the Proceedings Second Workshop on Trends in Functional Programming In Education, 2013

Static Contract Checking for Scripting Languages.

Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn

CoRR, 2013

Resolving and Exploiting the $k$-CFA Paradox.

Matthew Might, Yannis Smaragdakis, David Van Horn

CoRR, 2013

Deciding $k$CFA is complete for EXPTIME.

David Van Horn, Harry G. Mairson

CoRR, 2013

The Complexity of Flow Analysis in Higher-Order Languages.

David Van Horn

CoRR, 2013

Optimizing abstract abstract machines.

Dionna Amalie Glaze, Nicholas Labich, Matthew Might, David Van Horn

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Sound and precise malware analysis for android via pushdown reachability and entry-point saturation.

Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, David Van Horn

Proceedings of the SPSM'13, 2013

Realm of Racket - Learn to Program, One Game at a Time!

Matthias Felleisen, David Van Horn, Conrad Barski

No Starch Press, ISBN: 978-1-59327-491-7, 2013

2012

Systematic abstraction of abstract machines.

David Van Horn, Matthew Might

J. Funct. Program., 2012

Optimizing Abstract Abstract Machines

Dionna Amalie Glaze, Matthew Might, David Van Horn

CoRR, 2012

Higher-order symbolic execution via contracts.

Sam Tobin-Hochstadt, David Van Horn

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Introspective pushdown analysis of higher-order programs.

Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

2011

Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5).

Naoki Kobayashi, Luke Ong, David Van Horn

NII Shonan Meet. Rep., 2011

An Analytic Framework for JavaScript

David Van Horn, Matthew Might

CoRR, 2011

Semantic Solutions to Program Analysis Problems

Sam Tobin-Hochstadt, David Van Horn

CoRR, 2011

Modular Analysis via Specifications as Values

Sam Tobin-Hochstadt, David Van Horn

CoRR, 2011

Abstracting abstract machines: a systematic approach to higher-order program analysis.

David Van Horn, Matthew Might

Commun. ACM, 2011

A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs.

Matthew Might, David Van Horn

Proceedings of the Static Analysis - 18th International Symposium, 2011

2010

Stack-Summarizing Control-Flow Analysis of Higher-Order Programs

Christopher Earl, Matthew Might, David Van Horn

CoRR, 2010

Pushdown Control-Flow Analysis of Higher-Order Programs

Christopher Earl, Matthew Might, David Van Horn

CoRR, 2010

Evaluating Call-by-Need on the Control Stack.

Stephen Chang, David Van Horn, Matthias Felleisen

Proceedings of the Trends in Functional Programming - 11th International Symposium, 2010

Resolving and exploiting the <i>k</i>-CFA paradox: illuminating functional vs. object-oriented program analysis.

Matthew Might, Yannis Smaragdakis, David Van Horn

Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

Abstracting abstract machines.

David Van Horn, Matthew Might

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

2008

Types and trace effects of higher order programs.

Christian Skalka, Scott F. Smith, David Van Horn

J. Funct. Program., 2008

Flow Analysis, Linearity, and PTIME.

David Van Horn, Harry G. Mairson

Proceedings of the Static Analysis, 15th International Symposium, 2008

Deciding <i>k</i>CFA is complete for EXPTIME.

David Van Horn, Harry G. Mairson

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

2007

Relating complexity and precision in control flow analysis.

David Van Horn, Harry G. Mairson

Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, 2007

2005

A Type and Effect System for Flexible Abstract Interpretation of Java: (Extended Abstract).

Christian Skalka, Scott F. Smith, David Van Horn

Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, 2005