default search action
Adam Chlipala
Person information
- affiliation: MIT, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j21]Jason Gross
, Andres Erbsen
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. J. Autom. Reason. 68(3): 19 (2024) - [j20]Amanda Liu
A Verified Compiler for a Functional Tensor Language. Proc. ACM Program. Lang. 8(PLDI): 320-342 (2024) - [j19]Samuel Gruetter
Live Verification in an Interactive Proof Assistant. Proc. ACM Program. Lang. 8(PLDI): 1535-1558 (2024) - [j18]Andres Erbsen
Foundational Integration Verification of a Cryptographic Server. Proc. ACM Program. Lang. 8(PLDI): 1704-1729 (2024) - [c54]Atalay Mert Ileri, Nickolai Zeldovich, Adam Chlipala, M. Frans Kaashoek:
Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism. CSF 2024: 96-111 - [c53]Samuel Gruetter, Thomas Bourgeat, Adam Chlipala:
Verifying Software Emulation of an Unsupported Hardware Instruction. ITP 2024: 17:1-17:16 - 2023
- [j17]Thomas Bourgeat
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proc. ACM Program. Lang. 7(ICFP): 108-124 (2023) - [j16]Joel Kuepper
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. Proc. ACM Program. Lang. 7(PLDI): 1268-1292 (2023) - [j15]Arthur Charguéraud
Omnisemantics: Smooth Handling of Nondeterminism. ACM Trans. Program. Lang. Syst. 45(1): 5:1-5:43 (2023) - [c52]Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom:
CryptOpt: Automatic Optimization of Straightline Code. ICSE Companion 2023: 141-145 - [i12]Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala:
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. CoRR abs/2305.02521 (2023) - [i11]Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom:
CryptOpt: Automatic Optimization of Straightline Code. CoRR abs/2305.19586 (2023) - 2022
- [j14]Mohsen Lesani, Li-yao Xia
C4: verified transactional objects. Proc. ACM Program. Lang. 6(OOPSLA1): 1-31 (2022) - [j13]Mirai Ikebuchi, Andres Erbsen
Certifying derivation of state machines from coroutines. Proc. ACM Program. Lang. 6(POPL): 1-31 (2022) - [j12]Amanda Liu
Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM Program. Lang. 6(POPL): 1-28 (2022) - [c51]Joonwon Choi, Adam Chlipala, Arvind:
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. CAV (2) 2022: 317-339 - [c50]Timothy M. Braje, Alice R. Lee, Andrew Wagner
Adversary Safety by Construction in a Language of Cryptographic Protocols. CSF 2022: 412-427 - [c49]Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala:
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. ITP 2022: 17:1-17:18 - [c48]Jason Gross, Théo Zimmermann
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. ITP 2022: 18:1-18:18 - [c47]Clément Pit-Claudel
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. PLDI 2022: 918-933 - [i10]Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala:
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. CoRR abs/2202.13823 (2022) - [i9]Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala:
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. CoRR abs/2205.00862 (2022) - [i8]Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom:
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. CoRR abs/2211.10665 (2022) - 2021
- [j11]Adam Chlipala
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl). Proc. ACM Program. Lang. 5(ICFP): 1-28 (2021) - [c46]Clément Pit-Claudel
Effective simulation and debugging for a high-level hardware language using software compilers. ASPLOS 2021: 789-803 - [c45]Andres Erbsen
Integration verification across software and hardware for a simple embedded system. PLDI 2021: 604-619 - [i7]Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, Adam Chlipala:
A Multipurpose Formal RISC-V Specification. CoRR abs/2104.00762 (2021) - 2020
- [j10]Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala:
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54(1): 23-30 (2020) - [c44]Clément Pit-Claudel
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. IJCAR (2) 2020: 119-137 - [c43]Adam Chlipala:
Proof assistants at the hardware-software interface (invited talk). CPP 2020: 2 - [c42]Thomas Bourgeat
The essence of Bluespec: a core language for rule-based hardware design. PLDI 2020: 243-257
2010 – 2019
- 2019
- [j9]Thomas Grégoire, Adam Chlipala:
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. J. Autom. Reason. 62(2): 193-213 (2019) - [j8]Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3(ICFP): 82:1-82:29 (2019) - [c41]Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala:
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. IEEE Symposium on Security and Privacy 2019: 1202-1219 - 2018
- [j7]Antonis Stampoulis, Adam Chlipala:
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. Proc. ACM Program. Lang. 2(ICFP): 93:1-93:30 (2018) - [c40]Jason Gross, Andres Erbsen, Adam Chlipala:
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. ITP 2018: 289-305 - [c39]Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin:
Computable decision making on the reals and other spaces: via partiality and nondeterminism. LICS 2018: 859-868 - [c38]Atalay Mert Ileri
Proving confidentiality in a file system using DiskSec. OSDI 2018: 323-338 - [i6]Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala:
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. CoRR abs/1803.04870 (2018) - [i5]Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin:
Computable decision making on the reals and other spaces via partiality and nondeterminism. CoRR abs/1805.00468 (2018) - 2017
- [j6]Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, Daniel Ziegler:
Certifying a file system using crash hoare logic: correctness in the presence of crashes. Commun. ACM 60(4): 75-84 (2017) - [j5]Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind:
Kami: a platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang. 1(ICFP): 24:1-24:30 (2017) - [j4]Peng Wang, Di Wang
TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA): 79:1-79:26 (2017) - [c37]Ziv Scully
A program optimization for automatic database result caching. POPL 2017: 271-284 - [c36]Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel
The End of History? Using a Proof Assistant to Replace Language Design with Library Design. SNAPL 2017: 3:1-3:15 - [c35]Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri
Verifying a high-performance crash-safe file system using a tree specification. SOSP 2017: 270-286 - 2016
- [j3]Adam Chlipala:
Ur/Web: a simple model for programming the web. Commun. ACM 59(8): 93-100 (2016) - [c34]Thomas Grégoire, Adam Chlipala:
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. ITP 2016: 167-183 - [c33]Mohsen Lesani, Christian J. Bell, Adam Chlipala:
Chapar: certified causally consistent distributed key-value stores. POPL 2016: 357-370 - [c32]Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich:
Using Crash Hoare Logic for Certifying the FSCQ File System. USENIX ATC 2016 - [e1]Jeremy Avigad, Adam Chlipala:
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016. ACM 2016, ISBN 978-1-4503-4127-1 [contents] - 2015
- [c31]Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave:
Modular Deductive Verification of Multiprocessor Hardware Designs. CAV (2) 2015: 109-127 - [c30]Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, Nickolai Zeldovich:
Specifying Crash Safety for Storage Systems. HotOS 2015 - [c29]Adam Chlipala:
An optimizing compiler for a purely functional web-application language. ICFP 2015: 10-21 - [c28]Adam Chlipala:
Ur/Web: A Simple Model for Programming the Web. POPL 2015: 153-165 - [c27]Adam Chlipala:
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. POPL 2015: 609-622 - [c26]Benjamin Delaware, Clément Pit-Claudel
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. POPL 2015: 689-700 - [c25]Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich:
Using Crash Hoare logic for certifying the FSCQ file system. SOSP 2015: 18-37 - [i4]Adam Chlipala:
Proof engineering: implementation challenges in rigorously verified software. PLMW@POPL 2015: 8:1 - 2014
- [c24]Jason Gross, Adam Chlipala, David I. Spivak:
Experience Implementing a Performant Category-Theory Library in Coq. ITP 2014: 275-291 - [c23]Gregory Malecha
Compositional Computational Reflection. ITP 2014: 374-389 - [c22]Peng Wang, Santiago Cuéllar, Adam Chlipala:
Compiler verification meets cross-language linking via data abstraction. OOPSLA 2014: 675-690 - [c21]Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock:
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI 2014: 33-47 - [i3]Jason Gross, Adam Chlipala, David I. Spivak:
Experience Implementing a Performant Category-Theory Library in Coq. CoRR abs/1401.7694 (2014) - 2013
- [b1]Adam Chlipala:
Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press 2013, ISBN 978-0-262-02665-9, pp. I-XII, 1-424 - [c20]Thomas Braibant, Adam Chlipala:
Formal Verification of Hardware Synthesis. CAV 2013: 213-228 - [c19]Adam Chlipala:
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. ICFP 2013: 391-402 - [i2]Thomas Braibant, Adam Chlipala:
Formal Verification of Hardware Synthesis. CoRR abs/1301.4779 (2013) - [i1]Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, Edward Z. Yang:
MirrorShard: Proof by Computational Reflection with Verified Hints. CoRR abs/1305.6543 (2013) - 2011
- [c18]Adam Chlipala:
Mostly-automated verification of low-level programs in computational separation logic. PLDI 2011: 234-245 - 2010
- [j2]Adam Chlipala:
An Introduction to Programming and Proving with Dependent Types in Coq. J. Formaliz. Reason. 3(2): 1-93 (2010) - [c17]Adam Chlipala:
Foundational Program Verification in Coq with Automated Proofs. MSFP@ICFP 2010: 19 - [c16]Adam Chlipala:
Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. OSDI 2010: 105-118 - [c15]Adam Chlipala:
Ur: statically-typed metaprogramming with type-level record computation. PLDI 2010: 122-133 - [c14]Adam Chlipala:
A verified compiler for an impure functional language. POPL 2010: 93-106
2000 – 2009
- 2009
- [c13]Adam Chlipala, J. Gregory Malecha
Effective interactive proofs for higher-order imperative programs. ICFP 2009: 79-90 - 2008
- [j1]Adam Chlipala:
Modular development of certified program verifiers with a proof assistant, . J. Funct. Program. 18(5-6): 599-647 (2008) - [c12]Adam Chlipala:
Parametric higher-order abstract syntax for mechanized semantics. ICFP 2008: 143-156 - 2007
- [c11]Adam Chlipala:
A certified type-preserving compiler from lambda calculus to assembly language. PLDI 2007: 54-65 - 2006
- [c10]Adam Chlipala:
Modular development of certified program verifiers with a proof assistant. ICFP 2006: 160-171 - [c9]Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula:
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. VMCAI 2006: 174-189 - [c8]Adam Chlipala:
Position Paper: Thoughts on Programming with Proof Assistants. PLPV@IJCAR 2006: 17-21 - 2005
- [c7]Bor-Yuh Evan Chang
The open verifier framework for foundational verifiers. TLDI 2005: 1-12 - [c6]Adam Chlipala, Leaf Petersen, Robert Harper:
Strict bidirectional type checking. TLDI 2005: 71-78 - [c5]Bor-Yuh Evan Chang
Type-based verification of assembly language for compiler debugging. TLDI 2005: 91-102 - 2004
- [c4]Dirk Beyer
Generating Tests from Counterexamples. ICSE 2004: 326-335 - [c3]Dirk Beyer
Invited talk: the blast query language for software verification. PEPM 2004: 201-202 - [c2]Dirk Beyer
Invited talk: the blast query language for software verification. PPDP 2004: 1-2 - [c1]Dirk Beyer
The Blast Query Language for Software Verification.. SAS 2004: 2-18
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: