David Darais
@daviddarais Twitter Logo
@davdar Github Logo

University of Maryland
A.V. Williams Rm. 3452
8223 Paint Branch Dr.
College Park, MD 20742

I'm a PhD student in computer science supervised by David Van Horn. Within the field of programming languages I study program analysis, mechanized proofs, and their combination. I'm a member of the PLUM research group at University of Maryland, College Park.

Constructive Galois Connections

Recently I developed Constructive Galois Connections (w/Van Horn, ICFP 2016), which solves the open problem of effectively embedding Galois connections in a proof assistant. Our framework enables the design of mechanically verified static analyzers which are both sound and computable by construction. Our insight is to identify a restricted subset of Galois connections which are amenable to mechanization, and which also support the benefits of a general abstraction framework.

Abstracting Definitional Interpreters

Also recently I developed Abstracting Definitional Interpreters (w/Labich, Nguyễn and Van Horn, Preprint July 2016), a framework for designing static analyzers from big-step semantics and definitional interpreters. In particular, the pushdown property of the analysis is inherited from the precise call-return matching of the metalanguage, à la Reynolds. We achieve these results by combining big-step interpreters, monad transformers, and a novel fixpoint iteration strategy for higher-order definitional interpreters.

Galois Transformers

I developed Galois Transformers (w/Might and Van Horn, OOPSLA 2015), a compositional framework for building static analyzers. Our framework synthesizes large families of analyses and their proofs of soundness for free, while also supporting variations in path and flow sensitivity. We achieve these results by combining abstract interpretation, monad transformers and small-step monadic interpreters.





Professional Activities


Last updated July 9, 2016