David Van Horn

Registered user since Wed 31 Dec 2014

Name: David Van Horn

Bio: David Van Horn is an Assistant Professor in the Department of Computer Science and the Institute for Advanced Computer Studies (UMIACS) at the University of Maryland, College Park. His research interests are in programming languages and formal methods, where he works toward making the construction of reusable, trusted software components possible and effective. He publishes regularly in the flagship SIGPLAN conferences, POPL, PLDI, OOPSLA, and ICFP, and his work has been recognized with a National Science Foundation CAREER Award, a CRA Computing Innovation Fellowship, a Communications of the ACM Research Highlight, an OOPSLA Distinguished Paper Award, and several invitations to special issues of the Journal of Functional Programming devoted to ICFP. He is the co-author of “Realm of Racket,” an illustrated book on programming video games, written and illustrated with eight undergraduate students. He is devoted to broadening participation in computer science and is currently serving as Chair of the ACM SIGPLAN Programming Languages Mentoring Workshop @ ICFP.

Country: United States

Affiliation: University of Maryland

Personal website: https://www.cs.umd.edu/~dvanhorn/

Research interests: Programming languages

Contributions

PLDI 2021 Author of RbSyn: Type- and Effect-Guided Program Synthesis within the PLDI Research Papers-track
PLMW @ ICFP 2020 Speaker of Basic Mechanics of Operational Semantics within the PLMW @ ICFP 2020-track
POPL 2021 Author of Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification within the POPL-track
Committee Member in Program Committee within the POPL-track
PLMW @ ICFP 2019 Author of Welcome within the PLMW @ ICFP 2019-track
PLMW Co-Chair in Organizing Committee within the PLMW @ ICFP 2019-track
SPLASH 2019 Committee Member in Review Committee within the OOPSLA-track
PLDI 2019 Author of Size-Change Termination as a Contract within the PLDI Research Papers-track
Author of Type-Level Computations for Ruby Libraries within the PLDI Research Papers-track
PLMW @ ICFP 2018 Co-chair in Organizing Committee within the PLMW @ ICFP 2018-track
Haskell 2018 Author of Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) within the Haskell 2018-track
Scheme 2018 Author of From Scripting to Proving: Gradual Verification with a Scheme within the Scheme 2018-track
SPLASH 2018 Author of Gradual Liquid Type Inference within the OOPSLA-track
Author of Gradual Liquid Type Inference within the Artifacts-track
ICFP 2018 PLMW Co-Chair in Organizing Committee
Committee Member in External Review Committee within the Research Papers-track
Committee Member in Selection Committee within the Student Research Competition-track
PLDI 2018 Committee Member in Student Research Competition Committee
ICFP 2017 Author of Abstracting Definitional Interpreters within the Research Papers-track
POPL 2018 Author of Soft Contract Verification for Higher-order Stateful Programs within the Artifact Evaluation-track
Author of Soft Contract Verification for Higher-order Stateful Programs within the Research Papers-track
PLMW 2016 Committee Member in Speakers within the PLMW-track
Author of Basic Mechanics of Operational Semantics within the PLMW-track
POPL 2017 Committee Member in Program Committee within the POPL-track
GPCE 2016 Author of A Vision for Online Verification-Validation within the GPCE-track
ICFP 2016 Committee Member in External Review Committee within the Research Papers-track
Author of Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory within the Research Papers-track
Student Research Competition Chair in Organizing Committee
ECOOP 2016 Committee Member in Program Committee within the Research Track-track
SPLASH 2016 Committee Member in Program Committee within the Posters-track
POPL 2016 Author of T1: An Introduction to Redex with Abstracting Abstract Machines within the Tutorials-track
ERC member in External Reviewing Committee
ERC member in External Reviewing Committee within the Research Papers-track
Author of Pushdown Control-flow Analysis for Free within the Research Papers-track
Author of T1: An Introduction to Redex with Abstracting Abstract Machines(Advanced Material) within the Tutorials-track
ESOP 2015 Author of Running Probabilistic Programs Backwards within the ESOP-track
SPLASH 2015 Author of Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis within the OOPSLA-track
Author of Incremental Computation with Names within the OOPSLA Artifacts-track
Author of Incremental Computation with Names within the OOPSLA-track
PLDI 2015 Author of Relatively Complete Counterexamples for Higher-Order Programs within the Research Papers-track
DLS Presenter of Abstracting Abstract Control within the DLS-track
SPLASH 2012 Author of Higher-order symbolic execution via contracts within the OOPSLA Research Papers-track
Scheme 2011 Committee Member in Program Committee within the Scheme 2011-track