David Darais ⌁ Assistant Professor ⌁ Computer Science

David Darais
Assistant Professor
Computer Science
University of Vermont

82 University Place
Innovation Building, E456
Burlington, VT 05405

david.darais@uvm.edu
@daviddarais
@davdar Github Logo

★ I am looking for PhD students to work with me in programming languages, secure computation, and/or data privacy.

My research addresses problems in software reliability through advances in program analysis, computer-checkable proofs, and their combination. Recently I have been working on new programming languages for data privacy and secure computation. I help run the UVM PLAID Lab.

Teaching

Current Students

Chike Abuah (PhD co-advised)
Krystal Maughan (PhD co-advised)
Ryan Estes (PhD co-advised)

Jacob Wunder (BS co-advised)
Phillip Nguyen (BS co-advised)

Past Students

Kristin Mills (MS co-advised)
Tim Stevens (MS co-advised)

Adam Barson (BS)
Lindsey Stuntz (BS co-advised)
Ramy Koudsi (BS)

Publications

David Darais, Ian Sweet, Chang Liu, Michael Hicks.
A Language for Probabilistically Oblivious Computation.
Principles of Programming Languages (POPL). 2020. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.key] [slides.pdf]
Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffan Smolka, Nate Foster.
Proof Carrying Network Code.
Computer and Communications Security (CCS). 2019. ACM.
[pdf] [abstract] [bibtex] [ACM]
Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song.
Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy.
Object-oriented Programming, Systems, Languages, and Applications (OOPSLA). 2019. ACM.
«ACM SIGPLAN Distinguished Paper Award»
[pdf] [abstract] [bibtex] [ACM] [arXiv] [video]
David Darais, David Van Horn.
Constructive Galois Connections.
Journal of Functional Programming (JFP). 2019. Cambridge University Press.
[pdf] [abstract] [bibtex] [JFP] [arXiv]
David Darais, Nicholas Labich, Phúc C. Nguyễn, David Van Horn.
Abstracting Definitional Interpreters.
International Conference on Functional Programming (ICFP). 2017. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
David Darais, David Van Horn.
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
International Conference on Functional Programming (ICFP). 2016. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
David Darais, Matthew Might, David Van Horn.
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). 2015. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
Ilya Sergey, Dominique Divriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
Monadic Abstract Interpreters.
Programming Language Design and Implementation (PLDI). 2013. ACM.
[pdf] [abstract] [bibtex] [ACM]
Matthew Flatt, Ryan Culpepper, David Darais, Robert Bruce Findler.
Macros that Work Together: Compile-time bindings, partial expansion, and definition contexts.
Journal of Functional Programming (JFP). 2012. Cambridge University Press.
[pdf] [abstract] [bibtex] [ACM]
Matthew Might, David Darais, Daniel Spiewak.
Functional Pearl: Parsing with Derivatives.
International Conference on Functional Programming (ICFP). 2011. ACM.
[pdf] [abstract] [bibtex] [ACM]

Theses

David Darais.
Mechanizing Abstract Interpretation.
PHD Thesis. University of Maryland. 2017.
[pdf] [abstract] [slides.pdf] [slides.key]

Workshops

David Darais.
Compositional and Mechanically Verified Program Analyzers.
ECOOP Doctoral Symposium (ECOOP-DS). 2016.
[pdf] [abstract] [slides.pdf] [slides.key]

Drafts

Kristopher Micinski, David Darais, Thomas Gilray.
Abstracting Faceted Execution: Static Analysis of Dynamic Information-flow Control for Higher-order Languages.
Draft. July 2018.
[pdf] [abstract]
David Christiansen, David Darais, Weixi Ma.
The Final Pretty Printer.
Draft. May 2017.
[pdf] [abstract]

Talks

Data Privacy by Programming Language Design.
Tech Talk - Millennium Institute - Foundational Research on Data. University of Chile, Santiago, Chile. May, 2019.
[UChile] [IMFD] [abstract] [slides.pdf TBD] [slides.key TBD]
A Simple and Extensible Approach to Program Analysis.
International Federation for Information Processing Working Group 2.4 on Software Implementation Technology (IFIP WG2.4). Essex, Vermont, USA. Oct, 2017.
[abstract] [slides.pdf] [slides.key]
Abstracting Definitional Interpreters.
International Conference on Functional Programming (ICFP). Oxford, England. September, 2017.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
International Conference on Functional Programming (ICFP). Nara, Japan. September, 2016.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
Compositional and Mechanically Verified Program Analyzers.
ECOOP Doctoral Symposium (ECOOP-DS). Rome, Italy. July, 2016.
[pdf] [abstract] [slides.pdf] [slides.key]
Constructive Galois Connections.
New Jersey Programming Languages and Systems Seminar (NJPLS). Philadelphia, Pennsylvania, USA. May, 2016.
[slides.pdf] [slides.key]
Adventures in Abstract Interpretation.
Research Seminar. University of Utah. February, 2016.
[slides.pdf] [slides.key] [video]
Constructive Galois Connections: With Applications to Abstracting Gradual Typing.
Research Seminar. University of Chile. January, 2016.
[slides.pdf] [slides.key] [demo.agda]
Formally Verifying and Deriving Gradual Type Systems.
Class Presentation. University of Maryland CMSC 631. December, 2015.
[slides.pdf] [slides.key]
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). Pittsburgh, Pennsylvania, USA. October, 2015.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]

Professional Activities

Organizing (co-)Chair: OOPSLA SRC 2019, TyDe 2019, ECOOP DS 2017
Program Committee (PC): ICFP 2020, TyDe 2018, IFL 2018
External/Extended Review Committee (ERC): PLDI 2020, ICFP 2018
Video (co-)Chair: OOPSLA 2017; POPL 2017; PLDI 2017, 2016; ECOOP 2017, 2016; ICFP 2013
Posters Committee: ICFP SRC 2019 (+ judge); ECOOP 2019 Posters
Artifact Evaluation Committee (AEC): POPL 2016
Student Volunteer: POPL 2016, ICFP 2013 (chair)
Logo Designer: ICFP 2013

Short Bio

David Darais is an Assistant Professor at the University of Vermont. David's research focuses on tools for achieving reliable software in critical, security-sensitive, and privacy-sensitive systems. David received his BS, MS and PhD from University of Utah, Harvard University and University of Maryland.