@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{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},
note = {Conditionally accepted},

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/}
}