Adam Chlipala
Affiliations: MIT, USA
According to our database^{1},
Adam Chlipala
authored at least 70 papers
between 2004 and 2023.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis Dataset OtherLinks
Online presence:

on orcid.org
On csauthors.net:
Bibliography
2023
Proc. ACM Program. Lang., August, 2023
ACM Trans. Program. Lang. Syst., March, 2023
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.
Proc. ACM Program. Lang., 2023
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.
CoRR, 2023
Proceedings of the 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, 2023
2022
Proc. ACM Program. Lang., 2022
Proc. ACM Program. Lang., 2022
Proc. ACM Program. Lang., 2022
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.
CoRR, 2022
Relational compilation for performancecritical applications: extensible proofproducing translation of functional models into lowlevel code.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022
Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical CacheCoherence Protocols.
Proceedings of the Computer Aided Verification  34th International Conference, 2022
2021
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl).
Proc. ACM Program. Lang., 2021
CoRR, 2021
Integration verification across software and hardware for a simple embedded system.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021
Effective simulation and debugging for a highlevel hardware language using software compilers.
Proceedings of the ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2021
2020
Simple HighLevel Code For Cryptographic Arithmetic: With Proofs, Without Compromises.
ACM SIGOPS Oper. Syst. Rev., 2020
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs.
Proceedings of the Automated Reasoning  10th International Joint Conference, 2020
2019
Narcissus: correctbyconstruction derivation of decoders and encoders from binary formats.
Proc. ACM Program. Lang., 2019
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms.
J. Autom. Reason., 2019
2018
Prototyping a functional language using higherorder logic programming: a functional pearl on learning the ways of λProlog/Makam.
Proc. ACM Program. Lang., 2018
Narcissus: Deriving CorrectByConstruction Decoders and Encoders from Binary Formats.
CoRR, 2018
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018
Computable decision making on the reals and other spaces: via partiality and nondeterminism.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018
Reification by Parametricity  Fast Setup for Proof by Reflection, in Two Lines of Ltac.
Proceedings of the Interactive Theorem Proving  9th International Conference, 2018
2017
Proc. ACM Program. Lang., 2017
Kami: a platform for highlevel parametric hardware specification and its modular verification.
Proc. ACM Program. Lang., 2017
Certifying a file system using crash hoare logic: correctness in the presence of crashes.
Commun. ACM, 2017
Proceedings of the 26th Symposium on Operating Systems Principles, 2017
The End of History? Using a Proof Assistant to Replace Language Design with Library Design.
Proceedings of the 2nd Summit on Advances in Programming Languages, 2017
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017
2016
Commun. ACM, 2016
Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2016
2015
Proceedings of the 25th Symposium on Operating Systems Principles, 2015
Proceedings of the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2015
Proceedings of the Programming Languages Mentoring Workshop, 2015
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification.
Proceedings of the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2015
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015
Proceedings of the 15th Workshop on Hot Topics in Operating Systems, 2015
Proceedings of the Computer Aided Verification  27th International Conference, 2015
2014
Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014
Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014
Proceedings of the Interactive Theorem Proving  5th International Conference, 2014
Proceedings of the Interactive Theorem Proving  5th International Conference, 2014
2013
CoRR, 2013
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013
Proceedings of the Computer Aided Verification  25th International Conference, 2013
Certified Programming with Dependent Types  A Pragmatic Introduction to the Coq Proof Assistant.
MIT Press, ISBN: 9780262026659, 2013
2011
Mostlyautomated verification of lowlevel programs in computational separation logic.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011
2010
J. Formaliz. Reason., 2010
Proceedings of the 37th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2010
Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010
Static Checking of DynamicallyVarying Security Policies in DatabaseBacked Applications.
Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation, 2010
Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010
2009
Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009
2008
J. Funct. Program., 2008
Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008
2007
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007
2006
Proceedings of the Programming Languages meets Program Verification, 2006
A Framework for Certified Program Analysis and Its Applications to MobileCode Safety.
Proceedings of the Verification, 2006
2005
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005
2004
Proceedings of the Static Analysis, 11th International Symposium, 2004
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semanticsbased Program Manipulation, 2004
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004