@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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/papers/BlastICSE04/}
}

	

	

	@Article{CertVerJFP,
author = {Adam Chlipala},
title = {Modular Development of Certified Program Verifiers with a Proof Assistant},
journal = {Journal of Functional Programming},
note = {Accepted pending revision},
url = {http://www.cs.berkeley.edu/~adamc/papers/CertVerJFP/}
}

	

	

	@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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/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://www.cs.berkeley.edu/~adamc/papers/ChlipalaMS/}
}