Adam Chlipala
Orcid: 0000-0001-7085-9417Affiliations:
- MIT, USA
According to our database1,
Adam Chlipala
authored at least 76 papers
between 2004 and 2024.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis Dataset OtherLinks
Online presence:
-
on orcid.org
On csauthors.net:
Bibliography
2024
J. Autom. Reason., September, 2024
Proc. ACM Program. Lang., 2024
Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024
Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism.
Proceedings of the 37th IEEE Computer Security Foundations Symposium, 2024
Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024
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
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
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.
CoRR, 2022
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level 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 Cache-Coherence 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
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021
Effective simulation and debugging for a high-level 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 High-Level 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: correct-by-construction 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 higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam.
Proc. ACM Program. Lang., 2018
Narcissus: Deriving Correct-By-Construction 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 high-level 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
Proceedings of the 2016 USENIX Annual Technical Conference, 2016
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016
2015
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT 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 SIGPLAN-SIGACT 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
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: 978-0-262-02665-9, 2013
2011
Mostly-automated verification of low-level 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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010
Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010
Static Checking of Dynamically-Varying Security Policies in Database-Backed 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 Mobile-Code 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 Semantics-based Program Manipulation, 2004
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004