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.

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 w/Joe Near)
Krystal Maughan (PhD co-advised)
Ryan Estes (PhD co-advised)

Kristin Mills (MS w/Joe Near)

Jacob Wunder (BS w/Joe Near)
Phillip Nguyen (BS w/Joe Near)

Past Students

Tim Stevens (MS w/Joe Near+Chris Skalka)

Adam Barson (BS)
Lindsey Stuntz (BS w/Chris Skalka)
Ramy Koudsi (BS)

Publications

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.
(conditionally accepted) Object-oriented Programming, Systems, Languages, and Applications (OOPSLA). 2019. ACM.
[pdf (draft)] [abstract (draft)] [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, 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

David Darais, Ian Sweet, Chang Liu, Michael Hicks.
A Language for Probabilistically Oblivious Computation.
Draft. July 2019.
[pdf] [abstract]
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

Upcoming
- TyDe 2019: Co-chair
- ICFP SRC 2019: Program Committee (PC)
- OOPSLA SRC 2019: Co-chair
- ECOOP Posters 2019: Committee
Past
- ICFP 2018: External Review Committee (ERC)
- TyDe 2018: Program Committee (PC)
- IFL 2018: Program Committee (PC)
- SPLASH 2017: Video Co-Chair
- PLDI 2017: Video Chair
- ECOOP DS 2017: Co-chair
- ECOOP 2017: Video Chair
- POPL 2017: Video Co-Chair
- ECOOP 2016: Video Chair
- PLDI 2016: Video Co-Chair
- POPL 2016: Artifact Evaluation Committee (AEC), Student Volunteer
- ICFP 2013: Student Volunteer Chair, Video Chair, Logo Designer

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.