@Article{OmniTOPLAS23,
author = {Arthur Charguéraud and Adam Chlipala and Andres Erbsen and Samuel Gruetter},
title = {Omnisemantics: Smooth Handling of Nondeterminism},
volume = {Volume 45},
pages = {Article No. 5},
year = {2023},
journal = {ACM Transactions on Programming Languages and Systems},
url = {http://adam.chlipala.net/papers/OmniTOPLAS23/}
}

	@Article{StencilsJAR18,
author = {Thomas Gregoire and Adam Chlipala},
title = {Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms},
note = https://doi.org/10.1007/s10817-018-9451-y,
journal = {Journal of Automated Reasoning},
url = {http://adam.chlipala.net/papers/StencilsJAR18/}
}

	@Article{DeepSpecPT,
author = {Andrew W. Appel and Lennart Beringer and Adam Chlipala and Benjamin C. Pierce and Zhong Shao and Stephanie Weirich and Steve Zdancewic},
title = {The Science of Deep Specification},
note = 2017 375 20160331,
journal = {Philosophical Transactions of the Royal Society A},
url = {http://adam.chlipala.net/papers/DeepSpecPT/}
}

	@Article{FscqCACM,
author = {Tej Chajed and Haogang Chen and Adam Chlipala and Frans Kaashoek and Nickolai Zeldovich and Daniel Ziegler},
title = {Research Highlight: Certifying a File System using Crash Hoare Logic: Correctness in the Presence of Crashes},
volume = {60(4)},
pages = {75-84},
year = {2017},
journal = {Communications of the ACM},
url = {http://adam.chlipala.net/papers/FscqCACM/}
}

	@Article{UrWebCACM,
author = {Adam Chlipala},
title = {Research Highlight: Ur/Web: A Simple Model for Programming the Web},
volume = {59(8)},
pages = {93-100},
year = {2016},
journal = {Communications of the ACM},
url = {http://adam.chlipala.net/papers/UrWebCACM/}
}

	@Article{CpdtJFR,
author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in Coq},
volume = {3(2)},
pages = {1-93},
year = {2010},
journal = {Journal of Formalized Reasoning},
url = {http://adam.chlipala.net/papers/CpdtJFR/}
}

	@Article{CertVerJFP,
author = {Adam Chlipala},
title = {Modular Development of Certified Program Verifiers with a Proof Assistant},
volume = {18(5/6)},
pages = {599-647},
year = {2008},
journal = {Journal of Functional Programming},
url = {http://adam.chlipala.net/papers/CertVerJFP/}
}

    

    
      @InProceedings{MetricsCPP26,
author = {Andy Tockman and Pratap Singh and Andres Erbsen and Samuel Gruetter and Adam Chlipala},
title = {Foundational Verification of Running-Time Bounds for Interactive Programs},
booktitle = {CPP'26: Proceedings of the 15th International Conference on Certified Programs and Proofs},
month = jan,
year = {2026},
location = {Rennes, France},
url = {http://adam.chlipala.net/papers/MetricsCPP26/}
}

      @InProceedings{PyrosomeOOPSLA25,
author = {Dustin Jamner and Gabriel Kammer and Ritam Nag and Adam Chlipala},
title = {Pyrosome: Verified Compilation for Modular Metatheory},
booktitle = {OOPSLA'25: Proceedings of the 2025 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications},
month = oct,
year = {2025},
location = {Singapore},
url = {http://adam.chlipala.net/papers/PyrosomeOOPSLA25/}
}

      @InProceedings{TalCCS25,
author = {Shixin Song and Tingzhen Dong and Kosi Nwabueze and Julian Zanders and Andres Erbsen and Adam Chlipala and Mengjia Yan},
title = {Securing Cryptographic Software via Typed Assembly Language and a Hardware Extension},
booktitle = {CCS'25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security},
month = oct,
year = {2025},
location = {Taipei, Taiwan},
url = {http://adam.chlipala.net/papers/TalCCS25/}
}

      @InProceedings{TimingPLDI25,
author = {Owen Conoly and Andres Erbsen and Adam Chlipala},
title = {Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers},
booktitle = {PLDI'25: Proceedings of the 46th ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2025},
location = {Seoul, South Korea},
url = {http://adam.chlipala.net/papers/TimingPLDI25/}
}

	  @InProceedings{FjfjPLDI25,
author = {Thomas Bourgeat and Jiazheng Liu and Adam Chlipala and Arvind},
title = {Making Concurrent Hardware Verification Sequential},
booktitle = {PLDI'25: Proceedings of the 46th ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2025},
location = {Seoul, South Korea},
url = {http://adam.chlipala.net/papers/FjfjPLDI25/}
}

      @InProceedings{IsolationCCS24,
author = {Stella Lau and Thomas Bourgeat and Clément Pit-Claudel and Adam Chlipala},
title = {Specification and Verification of Strong Timing Isolation of Hardware Enclaves},
booktitle = {CCS'24: Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security},
month = oct,
year = {2024},
location = {Salt Lake City, UT, USA},
url = {http://adam.chlipala.net/papers/IsolationCCS24/}
}

      @InProceedings{UnsupportedITP24,
author = {Samuel Gruetter and Thomas Bourgeat and Adam Chlipala},
title = {Verifying Software Emulation of an Unsupported Hardware Instruction},
booktitle = {ITP'24: Proceedings of the Interactive Theorem Proving - Fifteenth International Conference},
month = sep,
year = {2024},
location = {Tbilisi, Georgia},
url = {http://adam.chlipala.net/papers/UnsupportedITP24/}
}

	  @InProceedings{ConFrmCSF24,
author = {Atalay Ileri and Nickolai Zeldovich and Adam Chlipala and Frans Kaashoek},
title = {Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism},
booktitle = {CSF'24: Proceedings of the 37th IEEE Computer Security Foundations Symposium},
month = jul,
year = {2024},
location = {Enschede, The Netherlands},
url = {http://adam.chlipala.net/papers/ConFrmCSF24/}
}

	  @InProceedings{GarageDoorPLDI24,
author = {Andres Erbsen and Jade Philipoom and Dustin Jamner and Ashley Lin and Samuel Gruetter and Clément Pit-Claudel and Adam Chlipala},
title = {Foundational Integration Verification of a Cryptographic Server},
booktitle = {PLDI'24: Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2024},
location = {Copenhagen, Denmark},
url = {http://adam.chlipala.net/papers/GarageDoorPLDI24/}
}

      @InProceedings{AtlPLDI24,
author = {Amanda Liu and Gilbert Bernstein and Adam Chlipala and Jonathan Ragan-Kelley},
title = {A Verified Compiler for a Functional Tensor Language},
booktitle = {PLDI'24: Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2024},
location = {Copenhagen, Denmark},
url = {http://adam.chlipala.net/papers/AtlPLDI24/}
}

      @InProceedings{LivePLDI24,
author = {Samuel Gruetter and Viktor Fukala and Adam Chlipala},
title = {Live Verification in an Interactive Proof Assistant},
booktitle = {PLDI'24: Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2024},
location = {Copenhagen, Denmark},
url = {http://adam.chlipala.net/papers/LivePLDI24/}
}

      @InProceedings{RiscvICFP23,
author = {Thomas Bourgeat and Ian Clester and Andres Erbsen and Samuel Gruetter and Pratap Singh and Andrew Wright and Adam Chlipala},
title = {Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)},
booktitle = {ICFP'23: Proceedings of the 28th ACM SIGPLAN International Conference on Functional Programming},
month = sep,
year = {2023},
location = {Seattle, WA, USA},
url = {http://adam.chlipala.net/papers/RiscvICFP23/}
}

      @InProceedings{CryptoptPLDI23,
author = {Joel Kuepper and Andres Erbsen and Jason Gross and Owen Conoly and Chuyue Sun and Samuel Tian and David Wu and Adam Chlipala and Chitchanok Chuengsatiansup and Daniel Genkin and Markus Wagner and Yuval Yarom},
title = {CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives},
booktitle = {PLDI'23: Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2023},
location = {Orlando, FL, USA},
url = {http://adam.chlipala.net/papers/CryptoptPLDI23/}
}

	  @InProceedings{TransactionsOOPSLA22,
author = {Mohsen Lesani and Li-yao Xia and Anders Kaseorg and Christian J. Bell and Adam Chlipala and Benjamin C. Pierce and Steve Zdancewic},
title = {C4: Verified Transactional Objects},
booktitle = {OOPSLA'22: Proceedings of the 2022 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications},
month = nov,
year = {2022},
location = {Auckland, New Zealand},
url = {http://adam.chlipala.net/papers/TransactionsOOPSLA22/}
}

      @InProceedings{HemiolaCAV22,
author = {Joonwon Choi and Adam Chlipala and Arvind},
title = {Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols},
booktitle = {CAV'22: Proceedings of the 34th International Conference on Computer-Aided Verification},
month = aug,
year = {2022},
location = {Haifa, Israel},
url = {http://adam.chlipala.net/papers/HemiolaCAV22/}
}

      @InProceedings{SpicyCSF22,
author = {Timothy Braje and Alice Lee and Andrew Wagner and Benjamin Kaiser and Daniel Park and Martine Kalke and Robert Cunningham and Adam Chlipala},
title = {Adversary Safety by Construction in a Language of Cryptographic Protocols},
booktitle = {CSF'22: Proceedings of the 35th IEEE Computer Security Foundations Symposium},
month = aug,
year = {2022},
location = {Haifa, Israel},
url = {http://adam.chlipala.net/papers/SpicyCSF22/}
}
          
      @InProceedings{RewriterITP22,
author = {Jason Gross and Andres Erbsen and Miraya Poddar-Agrawal and Jade Philipoom and Adam Chlipala},
title = {Accelerating Verified-Compiler Development with a Verified Rewriting Engine},
booktitle = {ITP'22: Proceedings of the Interactive Theorem Proving - Thirteenth International Conference},
month = aug,
year = {2022},
location = {Haifa, Israel},
url = {http://adam.chlipala.net/papers/RewriterITP22/}
}

      @InProceedings{MinimizerITP22,
author = {Jason Gross and Théo Zimmermann and Miraya Poddar-Agrawal and Adam Chlipala},
title = {Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq},
booktitle = {ITP'22: Proceedings of the Interactive Theorem Proving - Thirteenth International Conference},
month = aug,
year = {2022},
location = {Haifa, Israel},
url = {http://adam.chlipala.net/papers/MinimizerITP22/}
}

      @InProceedings{RupicolaPLDI22,
author = {Clément Pit-Claudel and Jade Philipoom and Dustin Jamner and Andres Erbsen and Adam Chlipala},
title = {Relational Compilation for Performance-Critical Applications},
booktitle = {PLDI'22: Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2022},
location = {San Diego, CA, USA},
url = {http://adam.chlipala.net/papers/RupicolaPLDI22/}
}

      @InProceedings{AtlPOPL22,
author = {Amanda Liu and Gilbert Bernstein and Adam Chlipala and Jonathan Ragan-Kelley},
title = {Verified Tensor-Program Optimization Via High-level Scheduling Rewrites},
booktitle = {POPL'22: Proceedings of the 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2022},
location = {Philadelphia, PA, USA},
url = {http://adam.chlipala.net/papers/AtlPOPL22/}
}

      @InProceedings{CoroutinesPOPL22,
author = {Mirai Ikebuchi and Andres Erbsen and Adam Chlipala},
title = {Certifying Derivation of State Machines from Coroutines},
booktitle = {POPL'22: Proceedings of the 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2022},
location = {Philadelphia, PA, USA},
url = {http://adam.chlipala.net/papers/CoroutinesPOPL22/}
}

      @InProceedings{FrapICFP21,
author = {Adam Chlipala},
title = {Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)},
booktitle = {ICFP'21: Proceedings of the 26th ACM SIGPLAN International Conference on Functional Programming},
month = aug,
year = {2021},
location = {Virtual},
url = {http://adam.chlipala.net/papers/FrapICFP21/}
}

      @InProceedings{LightbulbPLDI21,
author = {Andres Erbsen and Samuel Gruetter and Joonwon Choi and Clark Wood and Adam Chlipala},
title = {Integration Verification Across Software and Hardware for a Simple Embedded System},
booktitle = {PLDI'21: Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation},
month = jun,
year = {2021},
location = {Quebec City, QC, Canada},
url = {http://adam.chlipala.net/papers/LightbulbPLDI21/}
}

      @InProceedings{CuttlesimASPLOS21,
author = {Clément Pit-Claudel and Thomas Bourgeat and Stella Lau and Arvind and Adam Chlipala},
title = {Effective Simulation and Debugging for a High-Level Hardware Language Using Software Compilers},
booktitle = {ASPLOS'21: Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems},
month = apr,
year = {2021},
location = {virtual},
url = {http://adam.chlipala.net/papers/CuttlesimASPLOS21/}
}

	  @InProceedings{FiatIJCAR20,
author = {Clément Pit-Claudel and Peng Wang and Benjamin Delaware and Jason Gross and Adam Chlipala},
title = {Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs},
booktitle = {IJCAR'20: Proceedings of the 9th International Joint Conference on Automated Reasoning},
month = jun,
year = {2020},
location = {Paris, France},
url = {http://adam.chlipala.net/papers/FiatIJCAR20/}
}

	  @InProceedings{KoikaPLDI20,
author = {Thomas Bourgeat and Clément Pit-Claudel and Adam Chlipala and Arvind},
title = {The Essence of Bluespec: A Core Language for Rule-Based Hardware Design},
booktitle = {PLDI'20: Proceedings of the ACM SIGPLAN 2020 Conference on Programming Language Design and Implementation},
month = jun,
year = {2020},
location = {London, England},
url = {http://adam.chlipala.net/papers/KoikaPLDI20/}
}

      @InProceedings{NarcissusICFP19,
author = {Benjamin Delaware and Sorawit Suriyakarn and Clément Pit-Claudel and Qianchuan Ye and Adam Chlipala},
title = {Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats},
booktitle = {ICFP'19: Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming},
month = aug,
year = {2019},
location = {Berlin, Germany},
url = {http://adam.chlipala.net/papers/NarcissusICFP19/}
}
      
	  @InProceedings{FiatCryptoSP19,
author = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
title = {Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises},
booktitle = {S&P'19: Proceedings of the IEEE Symposium on Security & Privacy 2019},
month = may,
year = {2019},
location = {San Francisco, CA, USA},
url = {http://adam.chlipala.net/papers/FiatCryptoSP19/}
}

	  @InProceedings{HscGOMAC19,
author = {Adam Chlipala},
title = {Algorithmic Checking of Security Arguments for Microprocessors},
booktitle = {GOMACTech'19: Proceedings of the Annual GOMACTech Conference 2019},
month = mar,
year = {2019},
location = {Albuquerque, NM, USA},
url = {http://adam.chlipala.net/papers/HscGOMAC19/}
}
      
	  @InProceedings{FscqOSDI18,
author = {Atalay Ileri and Tej Chajed and Adam Chlipala and Frans Kaashoek and Nickolai Zeldovich},
title = {Proving confidentiality in a file system using DiskSec},
booktitle = {OSDI'18: Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation},
month = oct,
year = {2018},
location = {Carlsbad, CA, USA},
url = {http://adam.chlipala.net/papers/FscqOSDI18/}
}
      
	  @InProceedings{MakamICFP18,
author = {Antonis Stampoulis and Adam Chlipala},
title = {Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of Lambda-Prolog/Makam},
booktitle = {ICFP'18: Proceedings of the 23rd ACM SIGPLAN International Conference on Functional Programming},
month = sep,
year = {2018},
location = {Saint Louis, MO, USA},
url = {http://adam.chlipala.net/papers/MakamICFP18/}
}

	  @InProceedings{ComputableLICS18,
author = {Benjamin Sherman and Luke Sciarappa and Adam Chlipala and Michael Carbin},
title = {Computable decision-making on the reals and other spaces via partiality and nondeterminism},
booktitle = {LICS'18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
month = jul,
year = {2018},
location = {Oxford, UK},
url = {http://adam.chlipala.net/papers/ComputableLICS18/}
}

	  @InProceedings{ReificationITP18,
author = {Jason Gross and Andres Erbsen and Adam Chlipala},
title = {Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac},
booktitle = {ITP'18: Proceedings of the Interactive Theorem Proving - Ninth International Conference},
month = jul,
year = {2018},
location = {Oxford, UK},
url = {http://adam.chlipala.net/papers/ReificationITP18/}
}

	  @InProceedings{FscqSOSP17,
author = {Haogang Chen and Tej Chajed and Alex Konradi and Stephanie Wang and Atalay Ileri and Adam Chlipala and Frans Kaashoek and Nickolai Zeldovich},
title = {Verifying a High-Performance Crash-Safe File System Using a Tree Specification},
booktitle = {SOSP'17: Proceedings of the 26th ACM Symposium on Operating Systems Principles},
month = oct,
year = {2017},
location = {Shanghai, China},
url = {http://adam.chlipala.net/papers/FscqSOSP17/}
}

	  @InProceedings{TimlOOPSLA17,
author = {Peng Wang and Di Wang and Adam Chlipala},
title = {TiML: A Functional Language for Practical Complexity Analysis with Invariants},
booktitle = {OOPSLA'17: Proceedings of the 2017 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications},
month = oct,
year = {2017},
location = {Vancouver, BC, Canada},
url = {http://adam.chlipala.net/papers/TimlOOPSLA17/}
}

	  @InProceedings{KamiICFP17,
author = {Joonwon Choi and Muralidaran Vijayaraghavan and Benjamin Sherman and Adam Chlipala and Arvind},
title = {Kami: A Platform for High-Level Parametric Hardware Specification and its Modular Verification},
booktitle = {ICFP'17: Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming},
month = sep,
year = {2017},
location = {Oxford, UK},
url = {http://adam.chlipala.net/papers/KamiICFP17/}
}

	  @InProceedings{FiatSNAPL17,
author = {Adam Chlipala and Benjamin Delaware and Samuel Duchovni and Jason Gross and Clément Pit-Claudel and Sorawit Suriyakarn and Peng Wang and Katherine Ye},
title = {The End of History? Using a Proof Assistant to Replace Language Design with Library Design},
booktitle = {SNAPL'17: Proceedings of the The 2nd Summit oN Advances in Programming Languages},
month = may,
year = {2017},
location = {Asilomar, CA, USA},
url = {http://adam.chlipala.net/papers/FiatSNAPL17/}
}

	  @InProceedings{SqlcachePOPL17,
author = {Ziv Scully and Adam Chlipala},
title = {A Program Optimization for Automatic Database Result Caching},
booktitle = {POPL'17: Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2017},
location = {Paris, France},
url = {http://adam.chlipala.net/papers/SqlcachePOPL17/}
}

	  @InProceedings{StencilsITP16,
author = {Thomas Gregoire and Adam Chlipala},
title = {Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms},
booktitle = {ITP'16: Proceedings of the Interactive Theorem Proving - Seventh International Conference},
month = aug,
year = {2016},
location = {Nancy, France},
url = {http://adam.chlipala.net/papers/StencilsITP16/}
}

	  @InProceedings{ChaparPOPL16,
author = {Mohsen Lesani and Christian J. Bell and Adam Chlipala},
title = {Chapar: Certified Causally Consistent Distributed Key-Value Stores},
booktitle = {POPL'16: Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2016},
location = {St. Petersburg, FL, USA},
url = {http://adam.chlipala.net/papers/ChaparPOPL16/}
}

	  @InProceedings{FscqSOSP15,
author = {Haogang Chen and Daniel Ziegler and Tej Chajed and Adam Chlipala and Frans Kaashoek and Nickolai Zeldovich},
title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
booktitle = {SOSP'15: Proceedings of the 25th ACM Symposium on Operating Systems Principles},
month = oct,
year = {2015},
location = {Monterey, CA, USA},
url = {http://adam.chlipala.net/papers/FscqSOSP15/}
}

	  @InProceedings{UrWebICFP15,
author = {Adam Chlipala},
title = {An Optimizing Compiler for a Purely Functional Web-Application Language},
booktitle = {ICFP'15: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming},
month = aug,
year = {2015},
location = {Vancouver, BC, Canada},
url = {http://adam.chlipala.net/papers/UrWebICFP15/}
}

	  @InProceedings{BlueCAV15,
author = {Muralidaran Vijayaraghavan and Adam Chlipala and Arvind and Nirav Dave},
title = {Modular Deductive Verification of Multiprocessor Hardware Designs},
booktitle = {CAV'15: Proceedings of the 27th International Conference on Computer Aided Verification},
month = jul,
year = {2015},
location = {San Francisco, CA, USA},
url = {http://adam.chlipala.net/papers/BlueCAV15/}
}

	  @InProceedings{FiatPOPL15,
author = {Benjamin Delaware and Clément Pit-Claudel and Jason Gross and Adam Chlipala},
title = {Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant},
booktitle = {POPL'15: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2015},
location = {Mumbai, India},
url = {http://adam.chlipala.net/papers/FiatPOPL15/}
}

	  @InProceedings{UrWebPOPL15,
author = {Adam Chlipala},
title = {Ur/Web: A Simple Model for Programming the Web},
booktitle = {POPL'15: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2015},
location = {Mumbai, India},
url = {http://adam.chlipala.net/papers/UrWebPOPL15/}
}

	  @InProceedings{BedrockPOPL15,
author = {Adam Chlipala},
title = {From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification},
booktitle = {POPL'15: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2015},
location = {Mumbai, India},
url = {http://adam.chlipala.net/papers/BedrockPOPL15/}
}

	  @InProceedings{CitoOOPSLA14,
author = {Peng Wang and Santiago Cuellar and Adam Chlipala},
title = {Compiler Verification Meets Cross-Language Linking via Data Abstraction},
booktitle = {OOPSLA'14: Proceedings of the 2014 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications},
month = oct,
year = {2014},
location = {Portland, OR, USA},
url = {http://adam.chlipala.net/papers/CitoOOPSLA14/}
}

	  @InProceedings{JitkOSDI14,
author = {Xi Wang and David Lazar and Nickolai Zeldovich and Adam Chlipala and Zachary Tatlock},
title = {Jitk: A Trustworthy In-Kernel Interpreter Infrastructure},
booktitle = {OSDI'14: Proceedings of the 11th USENIX Symposium on Operating System Design and Implementation},
month = oct,
year = {2014},
location = {Broomfield, CO, USA},
url = {http://adam.chlipala.net/papers/JitkOSDI14/}
}

	  @InProceedings{MirrorShardITP14,
author = {Gregory Malecha and Adam Chlipala and Thomas Braibant},
title = {Compositional Computational Reflection},
booktitle = {ITP'14: Proceedings of the 5th International Conference on Interactive Theorem Proving},
month = jul,
year = {2014},
location = {Vienna, Austria},
url = {http://adam.chlipala.net/papers/MirrorShardITP14/}
}

	  @InProceedings{CategoryITP14,
author = {Jason Gross and Adam Chlipala and David Spivak},
title = {Experience Implementing a Performant Category-Theory Library in Coq},
booktitle = {ITP'14: Proceedings of the 5th International Conference on Interactive Theorem Proving},
month = jul,
year = {2014},
location = {Vienna, Austria},
url = {http://adam.chlipala.net/papers/CategoryITP14/}
}

	  @InProceedings{BedrockICFP13,
author = {Adam Chlipala},
title = {The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier},
booktitle = {ICFP'13: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
month = sep,
year = {2013},
location = {Boston, MA, USA},
url = {http://adam.chlipala.net/papers/BedrockICFP13/}
}

	  @InProceedings{FesiCAV13,
author = {Thomas Braibant and Adam Chlipala},
title = {Formal Verification of Hardware Synthesis},
booktitle = {CAV'13: Proceedings of the 25th International Conference on Computer Aided Verification},
month = jul,
year = {2013},
location = {Saint Petersburg, Russia},
url = {http://adam.chlipala.net/papers/FesiCAV13/}
}

	  @InProceedings{BedrockPLDI11,
author = {Adam Chlipala},
title = {Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic},
booktitle = {PLDI'11: Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation},
month = jun,
year = {2011},
location = {San Jose, CA, USA},
url = {http://adam.chlipala.net/papers/BedrockPLDI11/}
}

	  @InProceedings{UrFlowOSDI10,
author = {Adam Chlipala},
title = {Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications},
booktitle = {OSDI'10: Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation},
month = oct,
year = {2010},
location = {Vancouver, BC, Canada},
url = {http://adam.chlipala.net/papers/UrFlowOSDI10/}
}

	  @InProceedings{UrPLDI10,
author = {Adam Chlipala},
title = {Ur: Statically-Typed Metaprogramming with Type-Level Record Computation},
booktitle = {PLDI'10: Proceedings of the ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation},
month = jun,
year = {2010},
location = {Toronto, Canada},
url = {http://adam.chlipala.net/papers/UrPLDI10/}
}

	  @InProceedings{ImpurePOPL10,
author = {Adam Chlipala},
title = {A Verified Compiler for an Impure Functional Language},
booktitle = {POPL'10: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
month = jan,
year = {2010},
location = {Madrid, Spain},
url = {http://adam.chlipala.net/papers/ImpurePOPL10/}
}

	  @InProceedings{YnotICFP09,
author = {Adam Chlipala and Gregory Malecha and Greg Morrisett and Avraham Shinnar and Ryan Wisnesky},
title = {Effective Interactive Proofs for Higher-Order Imperative Programs},
booktitle = {ICFP'09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
month = aug,
year = {2009},
location = {Edinburgh, Scotland},
url = {http://adam.chlipala.net/papers/YnotICFP09/}
}

	  @InProceedings{PhoasICFP08,
author = {Adam Chlipala},
title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
booktitle = {ICFP'08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
month = sep,
year = {2008},
location = {Victoria, British Columbia, Canada},
url = {http://adam.chlipala.net/papers/PhoasICFP08/}
}

	  @InProceedings{CtpcPLDI07,
author = {Adam Chlipala},
title = {A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language},
booktitle = {PLDI'07: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation},
month = jun,
year = {2007},
location = {San Diego, California, USA},
url = {http://adam.chlipala.net/papers/CtpcPLDI07/}
}

	  @InProceedings{CertVerICFP06,
author = {Adam Chlipala},
title = {Modular Development of Certified Program Verifiers with a Proof Assistant},
booktitle = {ICFP'06: Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming},
month = sep,
year = {2006},
location = {Portland, Oregon, USA},
url = {http://adam.chlipala.net/papers/CertVerICFP06/}
}

	  @InProceedings{PcvVMCAI06,
author = {Bor-Yuh Evan Chang and Adam Chlipala and George C. Necula},
title = {A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety},
booktitle = {VMCAI'06: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation},
month = jan,
year = {2006},
location = {Charleston, South Carolina, USA},
url = {http://adam.chlipala.net/papers/PcvVMCAI06/}
}

	@InProceedings{BlastICSE04,
author = {Dirk Beyer and Adam J. Chlipala and Thomas Henzinger and Ranjit Jhala and Rupak Majumdar},
title = {Generating Tests from Counterexamples},
booktitle = {ICSE'04: Proceedings of the 26th International Conference on Software Engineering},
month = may,
year = {2004},
location = {Edinburgh, Scotland},
url = {http://adam.chlipala.net/papers/BlastICSE04/}
}

	

	

	@InProceedings{StorageHotOS15,
author = {Haogang Chen and Daniel Ziegler and Adam Chlipala and Frans Kaashoek and Eddie Kohler and Nickolai Zeldovich},
title = {Towards Certified Storage Systems},
booktitle = {HotOS'15: Proceedings of the 15th Workshop on Hot Topics in Operating Systems},
month = may,
year = {2015},
location = {Kartause Ittingen, Switzerland},
url = {http://adam.chlipala.net/papers/StorageHotOS15/}
}

	@InProceedings{PositionPLPV06,
author = {Adam Chlipala},
title = {Position Paper: Thoughts on Programming with Proof Assistants},
booktitle = {PLPV'06: Proceedings of the Programming Languages meets Program Verification Workshop},
month = aug,
year = {2006},
location = {Seattle, Washington, USA},
url = {http://adam.chlipala.net/papers/PositionPLPV06/}
}

	@InProceedings{KettleStrategies06,
author = {Adam Chlipala and George C. Necula},
title = {Cooperative Integration of an Interactive Proof Assistant and an Automated Prover},
booktitle = {STRATEGIES'06: Proceedings of the 6th International Workshop on Strategies in Automated Deduction},
month = aug,
year = {2006},
location = {Seattle, Washington, USA},
url = {http://adam.chlipala.net/papers/KettleStrategies06/}
}

	@InProceedings{OpenverTLDI05,
author = {Bor-Yuh Evan Chang and Adam Chlipala and George C. Necula and Robert R. Schneck},
title = {The {Open Verifier} Framework for Foundational Verifiers},
booktitle = {TLDI'05: Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation},
month = jan,
year = {2005},
location = {Long Beach, California, USA},
url = {http://adam.chlipala.net/papers/OpenverTLDI05/}
}

	@InProceedings{CoolaidTLDI05,
author = {Bor-Yuh Evan Chang and Adam Chlipala and George C. Necula and Robert R. Schneck},
title = {Type-Based Verification of Assembly Language for Compiler Debugging},
booktitle = {TLDI'05: Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation},
month = jan,
year = {2005},
location = {Long Beach, California, USA},
url = {http://adam.chlipala.net/papers/CoolaidTLDI05/}
}

	@InProceedings{StrictTLDI05,
author = {Adam Chlipala and Leaf Petersen and Robert Harper},
title = {Strict Bidirectional Type Checking},
booktitle = {TLDI'05: Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation},
month = jan,
year = {2005},
location = {Long Beach, California, USA},
url = {http://adam.chlipala.net/papers/StrictTLDI05/}
}

	

	

	@InProceedings{PosterPCC06,
author = {Adam Chlipala},
title = {Developing Certified Program Verifiers with a Proof Assistant},
booktitle = {PCC'06: Proceedings of the International Workshop on Proof-Carrying Code},
month = aug,
year = {2006},
location = {Seattle, Washington, USA},
url = {http://adam.chlipala.net/papers/PosterPCC06/}
}

	

	

	@InProceedings{BlastSAS04,
author = {Dirk Beyer and Adam J. Chlipala and Thomas Henzinger and Ranjit Jhala and Rupak Majumdar},
title = {The {Blast} Query Language for Software Verification},
booktitle = {SAS'04: Proceedings of the 11th Static Analysis Symposium},
month = aug,
year = {2004},
location = {Verona, Italy},
url = {http://adam.chlipala.net/papers/BlastSAS04/}
}

	

	

	@TechReport{AutoSyntaxTR,
author = {Adam Chlipala},
title = {Generic Programming and Proving for Programming Language Metatheory},
type = {{Technical Report}},
number = {UCB/EECS-2007-147},
year = {2007},
url = {http://adam.chlipala.net/papers/AutoSyntaxTR/}
}

	@TechReport{ChlipalaPhD,
author = {Adam Chlipala},
title = {Implementing Certified Programming Language Tools in Dependent Type Theory},
type = {{Technical Report}},
number = {UCB/EECS-2007-113},
year = {2007},
url = {http://adam.chlipala.net/papers/ChlipalaPhD/}
}

	@TechReport{LaconicTR,
author = {Adam Chlipala},
title = {Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types},
type = {{Technical Report}},
number = {UCB/EECS-2006-120},
year = {2006},
url = {http://adam.chlipala.net/papers/LaconicTR/}
}

	@TechReport{PcvTR,
author = {Bor-Yuh Evan Chang and Adam Chlipala and George C. Necula},
title = {A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety},
type = {{Technical Report}},
number = {UCB/ERL M05/32},
institution = {UC Berkeley EECS Department},
year = {2005},
url = {http://adam.chlipala.net/papers/PcvTR/}
}

	@TechReport{ChlipalaMS,
author = {Adam Chlipala},
title = {An Untrusted Verifier for Typed Assembly Language},
type = {{Technical Report}},
number = {UCB/ERL M04/41},
institution = {UC Berkeley EECS Department},
year = {2004},
url = {http://adam.chlipala.net/papers/ChlipalaMS/}
}