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

PLDI 2023 Committee Member in PLDI Review Committee within the PLDI Research Papers-track
PLARCH 2023 Co-chair in Organizing Committee within the PLARCH 2023-track
ICSE 2023 Author of CryptOpt: Automatic Optimization of Straightline Code within the DEMO - Demonstrations-track
CoqPL 2023 Author of Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation within the CoqPL 2023-track
CPP 2023 Session Chair of Formalized Mathematics I (part of CPP 2023)
Committee Member in Steering Committee within the CPP 2023-track
PEPM 2023 Author of Fast Cryptographic Code via Partial Evaluation within the PEPM 2023-track
SPLASH 2022 Author of C4: verified transactional objects within the OOPSLA-track
ICFP 2022 Committee Member in Steering Committee
PLDI 2022 Session Chair of Distributed Systems (part of SIGPLAN Track)
Author of Relational Compilation for Performance-Critical Applications within the PLDI-track
Author of (POPL 2022) Verified Tensor-Program Optimization Via High-level Scheduling Rewrites within the SIGPLAN Track-track
POPL 2022 Session Chair of Invited Talk (part of POPL)
Author of Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites within the POPL-track
Author of Virtualization Chair Report within the POPL-track
Virtualization Co-Chair in Organizing Committee
Co-chair in Selection Committee within the Virtual Workshop-track
Author of Certifying Derivation of State Machines from Coroutines within the POPL-track
CPP 2022 Committee Member in Steering Committee within the CPP 2022-track
SPLASH 2021 Author of Integration Verification Across Software and Hardware for a Simple Embedded System within the SIGPLAN Papers-track
ICFP 2020 PC Chair in Chairs within the SIGPLAN Papers-track
Author of The Essence of Bluespec: A Core Language for Rule-Based Hardware Design within the SIGPLAN Papers-track
ICFP 2021 Author of Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl) within the Research Papers-track
Massachusetts Institute of Technology in Steering Committee
Speaker of Ask Me Anything on Coq with Adam Chlipala within the Social Events-track
PLDI 2021 Committee Member in Program Committee within the PLDI-track
Author of Integration Verification across Software and Hardware for a Simple Embedded System within the PLDI-track
POPL 2021 Committee Member in Program Committee within the POPL-track
CPP 2021 Steering Committee Member in Steering Committee within the CPP 2021-track
CoqPL 2021 Author of Automated Synthesis of Verified Firewalls within the CoqPL-track
ICFP 2020 Session Chair of New York 1 (part of ICFP Program)
Committee Member in Virtualization Committee
Session Chair of Asia 1 (part of ICFP Program)
Session Chair of Keynote (part of ICFP Program)
Program Chair of Award Presentations & Chair Report within the ICFP Program-track
Program Chair in Program Committee within the ICFP Program-track
Committee Member in Selection Committee within the Tutorials-track
Program Chair in Organizing Committee
PLDI 2020 Author of The Essence of Bluespec: A Core Language for Rule-Based Hardware Design within the PLDI Research Papers-track
REMS-DeepSpec 2020 Author of The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System within the REMS-DeepSpec 2020-track
CPP 2020 Session Chair of Verified cryptography (part of CPP 2020)
Author of Invited talk: Proof Assistants at the Hardware-Software Interface within the CPP 2020-track
ICFP 2019 Committee 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)
DeepSpec 2019 Session 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
SPLASH 2018 Author 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 2018 Author 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
DeepSpec 2018 Speaker of Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels within the DeepSpec 2018-track
PLDI 2018 Session Chair of Verification (part of PLDI Research Papers)
Committee Member in Program Committee
SPLASH 2017 Author of TiML: A Functional Language for Practical Complexity Analysis with Invariants within the OOPSLA-track
Committee Member in Program Committee within the Workshops-track
ICFP 2017 Committee 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
DSW 2017 Committee 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 2017 Committee Member in External Review Committee
POPL 2017 Committee 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
RDP 2017 Author of Fiat: A New Take on Domain-Specific Languages by Programming with Specifications within the RDP-track
SPLASH 2016 Session 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
ICFP 2016 Committee Member in External Review Committee within the Research Papers-track
CoqPL 2016 Committee Member in Program Committee within the CoqPL-track
POPL 2016 Author of Certified Causally Consistent Distributed Key-Value Stores within the Research Papers-track
CPP 2016 Program Co-Chair in Program Committee within the CPP-track
PEPM 2016 Invited Speaker of Invited Talk: Fiat: Extensible Code Generation with Proofs within the Invited Talks-track
SPLASH 2015 Committee Member in Program Committee within the OOPSLA-track
ESOP 2015 Committee Member in Program Committee within the ESOP-track
SPLASH 2014 Author 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