Principal Scientist
Galois, Inc.
darais@galois.com | |
@daviddarais | |
@davdar | |
CV | |
when I'm free |
I'm currently a Principal Scientist at Galois, Inc.. 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 used to help run and still actively collaborate with the UVM PLAID Lab.
Publications
-
DuetSGX: Differential Privacy with Secure Hardware.
Phillip Nguyen, Alex Silence, David Darais and Joseph Near.
Theory and Practice of Differential Privacy (TPDP). 2020.
[pdf] [abstract] [bibtex] [arXiv] -
Short Paper: Probabilistically Almost-Oblivious Computation.
Ian Sweet, David Darais, Michael Hicks.
Programming Languages and Analysis for Security (PLAS). ACM, 2020.
[pdf] [abstract] [bibtex] [ACM] -
Types and Abstract Interpretation for Authorization Hook Advice.
Christian Skalka, David Darais, Trent Jaeger, Frank Capobianco.
Computer Security Foundations (CSF). IEEE, 2020.
[pdf] [abstract] [bibtex] [IEEE] -
Abstracting Faceted Execution.
Kristopher Micinski, David Darais, Thomas Gilray.
Computer Security Foundations (CSF). IEEE, 2020.
[pdf] [abstract] [bibtex] [IEEE] -
A Language for Probabilistically Oblivious Computation.
David Darais, Ian Sweet, Chang Liu, Michael Hicks.
Principles of Programming Languages (POPL). ACM, 2020.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.key] [slides.pdf] -
Proof Carrying Network Code.
Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffan Smolka, Nate Foster.
Computer and Communications Security (CCS). ACM, 2019.
[pdf] [abstract] [bibtex] [ACM] -
Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy.
Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song.
Object-oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2019.
«ACM SIGPLAN Distinguished Paper Award»
[pdf] [abstract] [bibtex] [ACM] [arXiv] [video] -
Constructive Galois Connections.
David Darais, David Van Horn.
Journal of Functional Programming (JFP). Cambridge University Press, 2019.
[pdf] [abstract] [bibtex] [JFP] [arXiv] -
Abstracting Definitional Interpreters.
David Darais, Nicholas Labich, Phúc C. Nguyễn, David Van Horn.
International Conference on Functional Programming (ICFP). ACM, 2017.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
David Darais, David Van Horn.
International Conference on Functional Programming (ICFP). ACM, 2016.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Compositional and Mechanically Verified Program Analyzers.
David Darais.
ECOOP Doctoral Symposium (ECOOP-DS). 2016.
[pdf] [abstract] [slides.pdf] [slides.key] -
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
David Darais, Matthew Might, David Van Horn.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). ACM, 2015.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Monadic Abstract Interpreters.
Ilya Sergey, Dominique Divriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
Programming Language Design and Implementation (PLDI). ACM, 2013.
[pdf] [abstract] [bibtex] [ACM] -
Macros that Work Together: Compile-time Bindings, Partial Expansion, and Definition Contexts.
Matthew Flatt, Ryan Culpepper, David Darais, Robert Bruce Findler.
Journal of Functional Programming (JFP). Cambridge University Press, 2012.
[pdf] [abstract] [bibtex] [ACM] -
Functional Pearl: Parsing with Derivatives.
Matthew Might, David Darais, Daniel Spiewak.
International Conference on Functional Programming (ICFP). ACM, 2011.
[pdf] [abstract] [bibtex] [ACM]
Theses
-
Mechanizing Abstract Interpretation.
David Darais.
PHD Thesis. University of Maryland. 2017.
[pdf] [abstract] [slides.pdf] [slides.key]
Drafts
-
The Final Pretty Printer.
David Christiansen, David Darais, Weixi Ma.
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
- NSF Panels: 1 SHF; (dates confidential)
- Steering Committee: TyDe 2020, 2021 (chair), 2022
- Organizing Chair: TyDe 2019 (co); OOPSLA SRC 2019 (co); ECOOP DS 2017 (co)
- Program Committee (PC): PLDI 2021; ICFP 2020; TyDe 2018; IFL 2018
- External/Extended Review Committee (ERC): PLDI 2020; ICFP 2018
- Posters Committee: ICFP SRC 2019 (+ judge); ECOOP 2019 Posters
- Mentoring Workshops: PLMS 2018 (panel)
- Video (co-)Chair: OOPSLA 2017; POPL 2017; PLDI 2017, 2016; ECOOP 2017, 2016; ICFP 2013
- Artifact Evaluation Committee (AEC): POPL 2016
- Student Volunteer: POPL 2016, ICFP 2013 (chair)
- Logo Designer: ICFP 2013

Teaching
- UVM CS 225: Programming Languages / Spring 2020
- 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)
- Ryan Estes (PhD co-advised)
Past Students
- Kristin Mills (MS co-advised)
- Tim Stevens (MS co-advised)
- Adam Barson (BS)
- Jacob Wunder (BS co-advised)
- Lindsey Stuntz (BS co-advised)
- Phillip Nguyen (BS co-advised)
- Ramy Koudsi (BS)
Short Bio
David is a Principal Scientist at Galois, Inc., where he builds programming languages and analysis tools which help programmers build reliable software. In particular, these languages and tools are designed for security-sensitive settings, and when applied, result in systems which are immune to large classes of defects. David received his BS from the University of Utah, MS from Harvard University, Ph.D. from the University of Maryland, and was previously an Assistant Professor at the University of Vermont before joining Galois.Medium Bio
David is a Principal Scientist at Galois, Inc., where he builds programming languages and analysis tools which help programmers build reliable software. In particular, these languages and tools are designed for security-sensitive settings, and when applied, result in systems which are immune to large classes of defects. David leverages state-of-the-art approaches, include program analysis, type checking, mechanized verification, differential privacy and secure multiparty computation. David considers a strong adversary when securing systems: the well-intended developer who accidentally misused security-relevant technology, such as cryptography or differential privacy. To combat this adversary, David co-designs programming languages in concert with verification tools to combat these defects, while also maintaining a usable, general-purpose programming environment for the developer. David received his BS from the University of Utah, MS from Harvard University, Ph.D. from the University of Maryland, and was previously an Assistant Professor at the University of Vermont before joining Galois.Links
- On Preparing Talks (by Ranjit Jhala at UCSD, ICFP PLMW 2018)
- How I Vim