Assistant Professor
Computer Science
University of Vermont
82 University Place
Innovation Building, E456
Burlington, VT 05405
david.darais@uvm.edu
@daviddarais

@davdar

★ 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
- ↯ UVM CS 295A: Software Verification / Fall 2019
- UVM CS 225: Programming Languages / Spring 2019
- UVM CS 295A: Software Verification / Fall 2018
- UVM CS 225: Programming Languages / Spring 2018
Current Students
- Chike Abuah (PhD co-advised)
- Krystal Maughan (PhD co-advised)
- Ryan Estes (PhD co-advised)
- Kristin Mills (MS co-advised)
- Jacob Wunder (BS co-advised)
- Phillip Nguyen (BS co-advised)
Past Students
- 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 (DRAFT)] [abstract (DRAFT)] [bibtex TBD] -
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 TBD] [abstract TBD] [bibtex TBD] -
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 TBD] -
David Darais, David Van Horn.
Constructive Galois Connections.
Journal of Functional Programming (JFP). 2019. Cambridge University Press.
[pdf] [abstract] [bibtex] [JFP] -
David Darais, Nicholas Labich, Phú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.Links
- On Preparing Talks (by Ranjit Jhala at UCSD, ICFP PLMW 2018)
- How I Vim