46 citations · 222 across the 24 of their papers we have counts for
4 papers · 1 filter
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais, David Van Horn
Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of…
Higher-order symbolic execution for contract verification and refutation
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. Our approach is sound an…
Pushdown Control-Flow Analysis for Free
Thomas Gilray, Steven Lyde, Michael D. Adams +2
Traditional control-flow analysis (CFA) for higher-order languages, whether implemented by constraint-solving or abstract interpretation, introduces spurious connections between ca…
Running Probabilistic Programs Backwards
Neil Toronto, Jay McCarthy, David Van Horn
Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other…