Adam Chlipala

Registered user since Sun 23 Nov 2014

Name: Adam Chlipala

Bio: Started hacking on compilers & web-development tools in the late 1990s. Finished CS undergrad at Carnegie Mellon in 2003 and CS PhD at Berkeley in 2007, picking up mechanized proof of executable, decently practical systems with Coq as a main focus in between. Postdoc at Harvard through 2011, then faculty at MIT since. Author of Certified Programming with Dependent Types, a popular online & in-print introduction to using Coq at scale. Lately into building practical but clean-slate hardware-software stacks with end-to-end Coq proofs of everything digital, at the same time as developing a startup-company idea to trick ordinary people into using dependent types (with Ur/Web) to generate their business applications.

Country: United States

Affiliation: Massachusetts Institute of Technology

Personal website: http://adam.chlipala.net/

Research interests: Programming Languages, Formal Methods, Computer Systems, Security

Contributions

ICFP 2020Program Chair in Program Committee within the Research Papers-track
Program Chair in Organizing Committee
CPP 2020Author of Invited talk: Proof Assistants at the Hardware-Software Interface within the CPP 2020-track
DeepSpec 2019Session Chair of HW/SW Interface Specifications (part of DeepSpec 2019)
Presenter of Project Updates from Participating Sites within the DeepSpec 2019-track
Presenter of Fast, Verified Partial Evaluation within the DeepSpec 2019-track
DeepSpec 2018Speaker of Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels within the DeepSpec 2018-track
ICFP 2019Committee Member in External Review Committee within the Research Papers-track
Author of Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats within the Research Papers-track
Session Chair of Program Verification (part of Research Papers)
SPLASH 2018Author of Nectry: Tricking End Users into Programming Practical Web Applications with Dependent Types within the Posters-track
Author of Mechanized Proofs of System Correctness in Production: Cryptography and Beyond within the SPLASH-I-track
Speaker in Speakers within the SPLASH-I-track
ICFP 2018Author of Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of ╬╗Prolog/Makam within the Research Papers-track
DSW 2017Committee Member in Organizing Committee within the DSW 2017-track
Author of Introduction to DeepSpec within the DSW 2017-track
Session Chair of Academic C-verification project; industry perspective on hypervisors (part of DSW 2017)
Author of Correct-by-Construction Generation of Fast Code for Elliptic Curves within the DSW 2017-track
PLDI 2018Session Chair of Verification (part of PLDI Research Papers)
Committee Member in Program Committee
ICFP 2017Committee Member in Program Committee within the Research Papers-track
Author of Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification within the Research Papers-track
RDP 2017Author of Fiat: A New Take on Domain-Specific Languages by Programming with Specifications within the RDP-track
POPL 2017Committee Member in Program Committee within the POPL-track
Session Chair of Concurrency 3 (part of POPL)
Author of A Program Optimization for Automatic Database Result Caching within the POPL-track
SPLASH 2017Author of TiML: A Functional Language for Practical Complexity Analysis with Invariants within the OOPSLA-track
Committee Member in Program Committee within the Workshops-track
PLDI 2017Committee Member in External Review Committee
ICFP 2016Committee Member in External Review Committee within the Research Papers-track
CoqPL 2016Committee Member in Program Committee within the CoqPL-track
PEPM 2016Invited Speaker of Invited Talk: Fiat: Extensible Code Generation with Proofs within the Invited Talks-track
CPP 2016Program Co-Chair in Program Committee within the CPP-track
SPLASH 2016Session Chair of Principles, Across the Compilation Stack (part of OOPSLA)
Speaker of Rapid Development of Web Applications with Typed Metaprogramming in Ur/Web within the SPLASH-I-track
POPL 2016Author of Certified Causally Consistent Distributed Key-Value Stores within the Research Papers-track
ESOP 2015Committee Member in Program Committee within the ESOP-track
SPLASH 2015Committee Member in Program Committee within the OOPSLA-track
SPLASH 2014Author of Compiler Verification Meets Cross-Language Linking via Data Abstraction within the OOPSLA-track
Presenter of Compiler Verification Meets Cross-Language Linking via Data Abstraction within the OOPSLA Artifacts-track