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