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/

GitHub:https://github.com/achlipala

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