default search action
David Van Horn
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [j13]Liyi Li
, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks:
A formal model of Checked C. J. Comput. Secur. 31(5): 581-614 (2023) - [j12]Sankha Narayan Guria
Absynthe: Abstract Interpretation-Guided Synthesis. Proc. ACM Program. Lang. 7(PLDI): 1584-1607 (2023) - [i44]Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn:
Absynthe: Abstract Interpretation-Guided Synthesis. CoRR abs/2302.13145 (2023) - 2022
- [c29]Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn
A Formal Model of Checked C. CSF 2022: 49-63 - [i43]Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks:
A Formal Model of Checked C. CoRR abs/2201.13394 (2022) - 2021
- [j11]Cameron Moy
Corpse reviver: sound and efficient gradual typing via contract verification. Proc. ACM Program. Lang. 5(POPL): 1-28 (2021) - [c28]Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
RbSyn: type- and effect-guided program synthesis. PLDI 2021: 344-358 - [i42]Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn:
RbSyn: Type- and Effect-Guided Program Synthesis. CoRR abs/2102.13183 (2021) - 2020
- [i41]Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn:
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification. CoRR abs/2007.12630 (2020)
2010 – 2019
- 2019
- [j10]David Darais, David Van Horn
Constructive Galois Connections. J. Funct. Program. 29: e11 (2019) - [c27]Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt
Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs. PLDI 2019: 845-859 - [c26]Milod Kazerounian, Sankha Narayan Guria, Niki Vazou
Type-level computations for Ruby libraries. PLDI 2019: 966-979 - [e2]David Van Horn
Trends in Functional Programming - 17th International Conference, TFP 2016, College Park, MD, USA, June 8-10, 2016, Revised Selected Papers. Lecture Notes in Computer Science 10447, Springer 2019, ISBN 978-3-030-14804-1 [contents] - [i40]Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn:
Type-Level Computations for Ruby Libraries. CoRR abs/1904.03521 (2019) - 2018
- [j9]Niki Vazou, Éric Tanter, David Van Horn
Gradual liquid type inference. Proc. ACM Program. Lang. 2(OOPSLA): 132:1-132:25 (2018) - [j8]Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt
Soft contract verification for higher-order stateful programs. Proc. ACM Program. Lang. 2(POPL): 51:1-51:30 (2018) - [c25]Niki Vazou
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). Haskell@ICFP 2018: 132-144 - [i39]Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton:
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). CoRR abs/1806.03541 (2018) - [i38]Niki Vazou, Éric Tanter, David Van Horn:
Gradual Liquid Type Inference. CoRR abs/1807.02132 (2018) - [i37]David Darais, David Van Horn:
Constructive Galois Connections. CoRR abs/1807.08711 (2018) - [i36]Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn:
Size-Change Termination as a Contract. CoRR abs/1808.02101 (2018) - 2017
- [j7]Phuc C. Nguyen, Sam Tobin-Hochstadt
Higher order symbolic execution for contract verification and refutation. J. Funct. Program. 27: e3 (2017) - [j6]David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn
Abstracting definitional interpreters (functional pearl). Proc. ACM Program. Lang. 1(ICFP): 12:1-12:25 (2017) - [i35]David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn:
Abstracting Definitional Interpreters. CoRR abs/1707.04755 (2017) - [i34]Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn:
Soft Contract Verification for Higher-Order Stateful Programs. CoRR abs/1711.03620 (2017) - 2016
- [c24]Matthew A. Hammer, Bor-Yuh Evan Chang
A vision for online verification-validation. GPCE 2016: 190-201 - [c23]David Darais, David Van Horn
Constructive Galois connections: taming the Galois connection framework for mechanized metatheory. ICFP 2016: 311-324 - [c22]Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn
Pushdown control-flow analysis for free. POPL 2016: 691-704 - [i33]Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn:
A Vision for Online Verification-Validation. CoRR abs/1608.06012 (2016) - 2015
- [j5]David Van Horn
The use of analytics in the design of sociotechnical products. Artif. Intell. Eng. Des. Anal. Manuf. 29(1): 65-81 (2015) - [c21]Neil Toronto, Jay McCarthy, David Van Horn:
Running Probabilistic Programs Backwards. ESOP 2015: 53-79 - [c20]David Darais, Matthew Might, David Van Horn
Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. OOPSLA 2015: 552-571 - [c19]Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks
Incremental computation with names. OOPSLA 2015: 748-766 - [c18]Phuc C. Nguyen, David Van Horn
Relatively complete counterexamples for higher-order programs. PLDI 2015: 446-456 - [i32]Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael Hicks, David Van Horn:
Incremental Computation with Names. CoRR abs/1503.07792 (2015) - [i31]Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn:
Pushdown Control-Flow Analysis for Free. CoRR abs/1507.03137 (2015) - [i30]David Darais, David Van Horn:
Mechanically Verified Calculational Abstract Interpretation. CoRR abs/1507.03559 (2015) - [i29]Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn:
Higher-order symbolic execution for contract verification and refutation. CoRR abs/1507.04817 (2015) - [i28]David Darais, David Van Horn:
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory. CoRR abs/1511.06965 (2015) - 2014
- [j4]Dionna Amalie Glaze, Ilya Sergey
Pushdown flow analysis with abstract garbage collection. J. Funct. Program. 24(2-3): 218-283 (2014) - [c17]Dionna Amalie Glaze, David Van Horn
Abstracting abstract control. DLS 2014: 11-22 - [c16]Phuc C. Nguyen, Sam Tobin-Hochstadt
Soft contract verification. ICFP 2014: 139-152 - [c15]Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn
Pruning, Pushdown Exception-Flow Analysis. SCAM 2014: 265-274 - [i27]Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn:
Pushdown flow analysis with abstract garbage collection. CoRR abs/1406.5106 (2014) - [i26]Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn:
Pruning, Pushdown Exception-Flow Analysis. CoRR abs/1409.3108 (2014) - [i25]David Darais, Matthew Might, David Van Horn:
Galois Transformers and Modular Abstract Interpreters. CoRR abs/1411.3962 (2014) - [i24]Phuc C. Nguyen, David Van Horn:
Relatively Complete Counterexamples for Higher-Order Programs. CoRR abs/1411.3967 (2014) - [i23]Neil Toronto, Jay McCarthy, David Van Horn:
Running Probabilistic Programs Backwards. CoRR abs/1412.4053 (2014) - 2013
- [b1]Matthias Felleisen, David Van Horn, Conrad Barski:
Realm of Racket - Learn to Program, One Game at a Time! No Starch Press 2013, ISBN 978-1-59327-491-7, pp. I-XVIII, 1-294 - [c14]Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous
Sound and precise malware analysis for android via pushdown reachability and entry-point saturation. SPSM@CCS 2013: 21-32 - [c13]Dionna Amalie Glaze, Nicholas Labich, Matthew Might, David Van Horn
Optimizing abstract abstract machines. ICFP 2013: 443-454 - [c12]Sam Tobin-Hochstadt
From Principles to Practice with Class in the First Year. TFPIE 2013: 1-15 - [c11]Shuying Liang, Matthew Might, David Van Horn
AnaDroid: Malware Analysis of Android with User-supplied Predicates. TAPAS@SAS 2013: 3-14 - [e1]Matthew Might, David Van Horn, Andreas Abel, Tim Sheard:
Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013. ACM 2013, ISBN 978-1-4503-1860-0 [contents] - [i22]Shuying Liang, Matthew Might, Thomas Gilray, David Van Horn:
Pushdown Exception-Flow Analysis of Object-Oriented Programs. CoRR abs/1302.2692 (2013) - [i21]Dionna Amalie Glaze, David Van Horn:
Concrete Semantics for Pushdown Analysis: The Essence of Summarization. CoRR abs/1305.3163 (2013) - [i20]Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn:
Static Contract Checking for Scripting Languages. CoRR abs/1307.6239 (2013) - [i19]Shuying Liang, Matthew Might, David Van Horn:
AnaDroid: Malware Analysis of Android with User-supplied Predicates. CoRR abs/1311.4198 (2013) - [i18]Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, David Van Horn:
Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. CoRR abs/1311.4201 (2013) - [i17]Matthew Might, Yannis Smaragdakis, David Van Horn:
Resolving and Exploiting the $k$-CFA Paradox. CoRR abs/1311.4231 (2013) - [i16]David Van Horn:
The Complexity of Flow Analysis in Higher-Order Languages. CoRR abs/1311.4733 (2013) - [i15]David Van Horn, Harry G. Mairson:
Deciding $k$CFA is complete for EXPTIME. CoRR abs/1311.5810 (2013) - [i14]David Van Horn, Harry G. Mairson:
Flow analysis, linearity, and PTIME. CoRR abs/1311.5825 (2013) - 2012
- [j3]David Van Horn
Systematic abstraction of abstract machines. J. Funct. Program. 22(4-5): 705-746 (2012) - [c10]Christopher Earl, Ilya Sergey
Introspective pushdown analysis of higher-order programs. ICFP 2012: 177-188 - [c9]Sam Tobin-Hochstadt
Higher-order symbolic execution via contracts. OOPSLA 2012: 537-554 - [i13]Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn:
Introspective Pushdown Analysis of Higher-Order Programs. CoRR abs/1207.1813 (2012) - [i12]Dionna Amalie Glaze, Matthew Might, David Van Horn:
Optimizing Abstract Abstract Machines. CoRR abs/1211.3722 (2012) - 2011
- [j2]David Van Horn
Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM 54(9): 101-109 (2011) - [c8]Matthew Might, David Van Horn:
A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. SAS 2011: 180-197 - [i11]Sam Tobin-Hochstadt, David Van Horn:
Modular Analysis via Specifications as Values. CoRR abs/1103.1362 (2011) - [i10]Matthew Might, David Van Horn:
A family of abstract interpretations for static analysis of concurrent higher-order programs. CoRR abs/1103.5167 (2011) - [i9]Sam Tobin-Hochstadt, David Van Horn:
Semantic Solutions to Program Analysis Problems. CoRR abs/1105.0106 (2011) - [i8]David Van Horn, Matthew Might:
Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis. CoRR abs/1105.1743 (2011) - [i7]David Van Horn, Matthew Might:
Systematic Abstraction of Abstract Machines. CoRR abs/1107.3539 (2011) - [i6]David Van Horn, Matthew Might:
An Analytic Framework for JavaScript. CoRR abs/1109.4467 (2011) - [i5]Naoki Kobayashi, Luke Ong, David Van Horn
Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). NII Shonan Meet. Rep. 2011 (2011) - 2010
- [c7]David Van Horn
Abstracting abstract machines. ICFP 2010: 51-62 - [c6]Matthew Might, Yannis Smaragdakis, David Van Horn
Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. PLDI 2010: 305-315 - [c5]Stephen Chang, David Van Horn, Matthias Felleisen:
Evaluating Call-by-Need on the Control Stack. Trends in Functional Programming 2010: 1-15 - [i4]Christopher Earl, Matthew Might, David Van Horn:
Pushdown Control-Flow Analysis of Higher-Order Programs. CoRR abs/1007.4268 (2010) - [i3]David Van Horn, Matthew Might:
Abstracting Abstract Machines. CoRR abs/1007.4446 (2010) - [i2]Christopher Earl, Matthew Might, David Van Horn:
Stack-Summarizing Control-Flow Analysis of Higher-Order Programs. CoRR abs/1009.1560 (2010) - [i1]Stephen Chang, David Van Horn, Matthias Felleisen:
Evaluating Call-By-Need on the Control Stack. CoRR abs/1009.3174 (2010)
2000 – 2009
- 2008
- [j1]Christian Skalka, Scott F. Smith, David Van Horn
Types and trace effects of higher order programs. J. Funct. Program. 18(2): 179-249 (2008) - [c4]David Van Horn
Deciding kCFA is complete for EXPTIME. ICFP 2008: 275-282 - [c3]David Van Horn, Harry G. Mairson:
Flow Analysis, Linearity, and PTIME. SAS 2008: 255-269 - 2007
- [c2]David Van Horn
Relating complexity and precision in control flow analysis. ICFP 2007: 85-96 - 2005
- [c1]Christian Skalka, Scott F. Smith, David Van Horn
A Type and Effect System for Flexible Abstract Interpretation of Java: (Extended Abstract). AIOOL@VMCAI 2005: 111-124
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: