@inproceedings{ChangCNS05,
  title = {The open verifier framework for foundational verifiers},
  author = {Bor-Yuh Evan Chang and Adam J. Chlipala and George C. Necula and Robert R. Schneck},
  year = {2005},
  doi = {10.1145/1040294.1040295},
  url = {http://doi.acm.org/10.1145/1040294.1040295},
  tags = {source-to-source, C++, open-source},
  researchr = {https://researchr.org/publication/ChangCNS05},
  cites = {0},
  citedby = {0},
  pages = {1-12},
  booktitle = {Proceedings of TLDI 05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005},
  editor = {J. Gregory Morrisett and Manuel Fähndrich},
  publisher = {ACM},
  isbn = {1-58113-999-3},
}

@inproceedings{MalechaCB14,
  title = {Compositional Computational Reflection},
  author = {Gregory Malecha and Adam J. Chlipala and Thomas Braibant},
  year = {2014},
  doi = {10.1007/978-3-319-08970-6_24},
  url = {http://dx.doi.org/10.1007/978-3-319-08970-6_24},
  researchr = {https://researchr.org/publication/MalechaCB14},
  cites = {0},
  citedby = {0},
  pages = {374-389},
  booktitle = {Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
  editor = {Gerwin Klein and Ruben Gamboa},
  volume = {8558},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-08969-0},
}

@inproceedings{Chlipala13,
  title = {The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier},
  author = {Adam J. Chlipala},
  year = {2013},
  doi = {10.1145/2500365.2500592},
  url = {http://doi.acm.org/10.1145/2500365.2500592},
  researchr = {https://researchr.org/publication/Chlipala13},
  cites = {0},
  citedby = {0},
  pages = {391-402},
  booktitle = {ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013},
  editor = {Greg Morrisett and Tarmo Uustalu},
  publisher = {ACM},
  isbn = {978-1-4503-2326-0},
}

@inproceedings{BraibantC13,
  title = {Formal Verification of Hardware Synthesis},
  author = {Thomas Braibant and Adam J. Chlipala},
  year = {2013},
  doi = {10.1007/978-3-642-39799-8_14},
  url = {http://dx.doi.org/10.1007/978-3-642-39799-8_14},
  researchr = {https://researchr.org/publication/BraibantC13},
  cites = {0},
  citedby = {0},
  pages = {213-228},
  booktitle = {Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  editor = {Natasha Sharygina and Helmut Veith},
  volume = {8044},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-39798-1},
}

@inproceedings{BeyerCHJM04:0,
  title = {Invited talk: the blast query language for software verification},
  author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
  year = {2004},
  doi = {10.1145/1013963.1013964},
  url = {http://doi.acm.org/10.1145/1013963.1013964},
  tags = {query language},
  researchr = {https://researchr.org/publication/BeyerCHJM04%3A0},
  cites = {0},
  citedby = {0},
  pages = {1-2},
  booktitle = {Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 24-26 August 2004, Verona, Italy},
  editor = {Eugenio Moggi and David Scott Warren},
  publisher = {ACM},
  isbn = {1-58113-819-9},
}

@inproceedings{Chlipala11,
  title = {Mostly-automated verification of low-level programs in computational separation logic},
  author = {Adam J. Chlipala},
  year = {2011},
  doi = {10.1145/1993498.1993526},
  url = {http://doi.acm.org/10.1145/1993498.1993526},
  researchr = {https://researchr.org/publication/Chlipala11},
  cites = {0},
  citedby = {0},
  pages = {234-245},
  booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011},
  editor = {Mary W. Hall and David A. Padua},
  publisher = {ACM},
  isbn = {978-1-4503-0663-8},
}

@inproceedings{Chlipala10-1,
  title = {Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications},
  author = {Adam J. Chlipala},
  year = {2010},
  url = {http://www.usenix.org/events/osdi10/tech/full_papers/Chlipala.pdf},
  researchr = {https://researchr.org/publication/Chlipala10-1},
  cites = {0},
  citedby = {0},
  pages = {105-118},
  booktitle = {9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010,  October 4-6, 2010, Vancouver, BC, Canada, Proceedings},
  editor = {Remzi H. Arpaci-Dusseau and Brad Chen},
  publisher = {USENIX Association},
  isbn = {978-1-931971-79-9},
}

@inproceedings{Chlipala07,
  title = {A certified type-preserving compiler from lambda calculus to assembly language},
  author = {Adam J. Chlipala},
  year = {2007},
  doi = {10.1145/1250734.1250742},
  url = {http://doi.acm.org/10.1145/1250734.1250742},
  tags = {compiler},
  researchr = {https://researchr.org/publication/Chlipala07},
  cites = {0},
  citedby = {0},
  pages = {54-65},
  booktitle = {Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007},
  editor = {Jeanne Ferrante and Kathryn S. McKinley},
  publisher = {ACM},
  isbn = {978-1-59593-633-2},
}

@inproceedings{ChangCNS05a,
  title = {Type-based verification of assembly language for compiler debugging},
  author = {Bor-Yuh Evan Chang and Adam J. Chlipala and George C. Necula and Robert R. Schneck},
  year = {2005},
  doi = {10.1145/1040294.1040303},
  url = {http://doi.acm.org/10.1145/1040294.1040303},
  tags = {rule-based, C++, debugging, compiler},
  researchr = {https://researchr.org/publication/ChangCNS05a},
  cites = {0},
  citedby = {0},
  pages = {91-102},
  booktitle = {Proceedings of TLDI 05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005},
  editor = {J. Gregory Morrisett and Manuel Fähndrich},
  publisher = {ACM},
  isbn = {1-58113-999-3},
}

@article{Chlipala07:0,
  title = {Position Paper: Thoughts on Programming with Proof Assistants},
  author = {Adam J. Chlipala},
  year = {2007},
  doi = {10.1016/j.entcs.2006.10.035},
  url = {http://dx.doi.org/10.1016/j.entcs.2006.10.035},
  tags = {proof assistant, programming},
  researchr = {https://researchr.org/publication/Chlipala07%3A0},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {174},
  number = {7},
  pages = {17-21},
}

@inproceedings{ChlipalaMMSW09,
  title = {Effective interactive proofs for higher-order imperative programs},
  author = {Adam J. Chlipala and J. Gregory Malecha and Greg Morrisett and Avraham Shinnar and Ryan Wisnesky},
  year = {2009},
  doi = {10.1145/1596550.1596565},
  url = {http://doi.acm.org/10.1145/1596550.1596565},
  researchr = {https://researchr.org/publication/ChlipalaMMSW09},
  cites = {0},
  citedby = {0},
  pages = {79-90},
  booktitle = {Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009},
  editor = {Graham Hutton and Andrew P. Tolmach},
  publisher = {ACM},
  isbn = {978-1-60558-332-7},
}

@inproceedings{GrossCS14,
  title = {Experience Implementing a Performant Category-Theory Library in Coq},
  author = {Jason Gross and Adam J. Chlipala and David I. Spivak},
  year = {2014},
  doi = {10.1007/978-3-319-08970-6_18},
  url = {http://dx.doi.org/10.1007/978-3-319-08970-6_18},
  researchr = {https://researchr.org/publication/GrossCS14},
  cites = {0},
  citedby = {0},
  pages = {275-291},
  booktitle = {Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
  editor = {Gerwin Klein and Ruben Gamboa},
  volume = {8558},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-08969-0},
}

@inproceedings{Chlipala10,
  title = {A verified compiler for an impure functional language},
  author = {Adam J. Chlipala},
  year = {2010},
  doi = {10.1145/1706299.1706312},
  url = {http://doi.acm.org/10.1145/1706299.1706312},
  tags = {programming languages, optimization, semantics, rule-based, translation, meta programming, proof assistant, program verification, exceptions, meta-model, abstract syntax, functional programming, reuse, source-to-source, logic programming, compiler,  mutable objects, programming, operational semantics, logic, type theory, program optimization, Meta-Environment, systematic-approach, open-source, meta-objects},
  researchr = {https://researchr.org/publication/Chlipala10},
  cites = {0},
  citedby = {0},
  pages = {93-106},
  booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010},
  editor = {Manuel V. Hermenegildo and Jens Palsberg},
  publisher = {ACM},
  isbn = {978-1-60558-479-9},
}

@inproceedings{Chlipala10-0,
  title = {Ur: statically-typed metaprogramming with type-level record computation},
  author = {Adam J. Chlipala},
  year = {2010},
  doi = {10.1145/1806596.1806612},
  url = {http://doi.acm.org/10.1145/1806596.1806612},
  researchr = {https://researchr.org/publication/Chlipala10-0},
  cites = {0},
  citedby = {1},
  pages = {122-133},
  booktitle = {Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010},
  editor = {Benjamin G. Zorn and Alexander Aiken},
  publisher = {ACM},
  isbn = {978-1-4503-0019-3},
}

@inproceedings{Chlipala08,
  title = {Parametric higher-order abstract syntax for mechanized semantics},
  author = {Adam J. Chlipala},
  year = {2008},
  doi = {10.1145/1411204.1411226},
  url = {http://doi.acm.org/10.1145/1411204.1411226},
  tags = {semantics, abstract syntax},
  researchr = {https://researchr.org/publication/Chlipala08},
  cites = {0},
  citedby = {0},
  pages = {143-156},
  booktitle = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008},
  editor = {James Hook and Peter Thiemann},
  publisher = {ACM},
  isbn = {978-1-59593-919-7},
}

@inproceedings{ChlipalaPH05,
  title = {Strict bidirectional type checking},
  author = {Adam J. Chlipala and Leaf Petersen and Robert Harper},
  year = {2005},
  doi = {10.1145/1040294.1040301},
  url = {http://doi.acm.org/10.1145/1040294.1040301},
  tags = {type checking},
  researchr = {https://researchr.org/publication/ChlipalaPH05},
  cites = {0},
  citedby = {0},
  pages = {71-78},
  booktitle = {Proceedings of TLDI 05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005},
  editor = {J. Gregory Morrisett and Manuel Fähndrich},
  publisher = {ACM},
  isbn = {1-58113-999-3},
}

@article{Chlipala10-2,
  title = {An Introduction to Programming and Proving with Dependent Types in Coq},
  author = {Adam J. Chlipala},
  year = {2010},
  doi = {10.6092/issn.1972-5787/1978},
  url = {http://dx.doi.org/10.6092/issn.1972-5787/1978},
  researchr = {https://researchr.org/publication/Chlipala10-2},
  cites = {0},
  citedby = {0},
  journal = {J. Formalized Reasoning},
  volume = {3},
  number = {2},
  pages = {1-93},
}

@inproceedings{BeyerCM04,
  title = {Generating Tests from Counterexamples},
  author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
  year = {2004},
  url = {http://csdl.computer.org/comp/proceedings/icse/2004/2163/00/21630326abs.htm},
  tags = {testing},
  researchr = {https://researchr.org/publication/BeyerCM04},
  cites = {0},
  citedby = {0},
  pages = {326-335},
  booktitle = {26th International Conference on Software Engineering (ICSE 2004), 23-28 May 2004, Edinburgh, United Kingdom},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-2163-0},
}

@inproceedings{BeyerCHJM04,
  title = {Invited talk: the blast query language for software verification},
  author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
  year = {2004},
  doi = {10.1145/1014007.1014028},
  url = {http://doi.acm.org/10.1145/1014007.1014028},
  tags = {query language},
  researchr = {https://researchr.org/publication/BeyerCHJM04},
  cites = {0},
  citedby = {0},
  pages = {201-202},
  booktitle = {Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004, Verona, Italy, August 24-25, 2004},
  editor = {Nevin Heintze and Peter Sestoft},
  publisher = {ACM},
  isbn = {1-58113-835-0},
}

@article{Chlipala08:0,
  title = {Modular development of certified program verifiers with a proof assistant, },
  author = {Adam J. Chlipala},
  year = {2008},
  doi = {10.1017/S0956796808006904},
  url = {http://dx.doi.org/10.1017/S0956796808006904},
  tags = {proof assistant, program verification},
  researchr = {https://researchr.org/publication/Chlipala08%3A0},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {18},
  number = {5-6},
  pages = {599-647},
}

@inproceedings{Chlipala06,
  title = {Modular development of certified program verifiers with a proof assistant},
  author = {Adam J. Chlipala},
  year = {2006},
  doi = {10.1145/1159803.1159825},
  url = {http://doi.acm.org/10.1145/1159803.1159825},
  tags = {proof assistant, program verification},
  researchr = {https://researchr.org/publication/Chlipala06},
  cites = {0},
  citedby = {0},
  pages = {160-171},
  booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006},
  editor = {John H. Reppy and Julia L. Lawall},
  publisher = {ACM},
  isbn = {1-59593-309-3},
}

@inproceedings{BeyerCHJM04:1,
  title = {The Blast Query Language for Software Verification.},
  author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3148&spage=2},
  tags = {query language},
  researchr = {https://researchr.org/publication/BeyerCHJM04%3A1},
  cites = {0},
  citedby = {0},
  pages = {2-18},
  booktitle = {Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings},
  editor = {Roberto Giacobazzi},
  volume = {3148},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22791-1},
}

@inproceedings{ChangCN06,
  title = {A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety},
  author = {Bor-Yuh Evan Chang and Adam J. Chlipala and George C. Necula},
  year = {2006},
  doi = {10.1007/11609773_12},
  url = {http://dx.doi.org/10.1007/11609773_12},
  tags = {program analysis, application framework, analysis, mobile code, C++, mobile},
  researchr = {https://researchr.org/publication/ChangCN06},
  cites = {0},
  citedby = {0},
  pages = {174-189},
  booktitle = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings},
  editor = {E. Allen Emerson and Kedar S. Namjoshi},
  volume = {3855},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-31139-4},
}