publications:
- title: "The open verifier framework for foundational verifiers"
  author:
  - name: "Bor-Yuh Evan Chang"
    link: "https://researchr.org/alias/bor-yuh-evan-chang"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "George C. Necula"
    link: "https://researchr.org/alias/george-c.-necula"
  - name: "Robert R. Schneck"
    link: "https://researchr.org/alias/robert-r.-schneck"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1040294.1040295"
  links:
    doi: "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: "tldi"
  kind: "inproceedings"
  key: "ChangCNS05"
- title: "Compositional Computational Reflection"
  author:
  - name: "Gregory Malecha"
    link: "https://researchr.org/alias/gregory-malecha"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Thomas Braibant"
    link: "https://researchr.org/alias/thomas-braibant"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_24"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_24"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/MalechaCB14"
  researchr: "https://researchr.org/publication/MalechaCB14"
  cites: 0
  citedby: 0
  pages: "374-389"
  booktitle: "itp"
  kind: "inproceedings"
  key: "MalechaCB14"
- title: "The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2500365.2500592"
  links:
    doi: "http://doi.acm.org/10.1145/2500365.2500592"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Chlipala13"
  researchr: "https://researchr.org/publication/Chlipala13"
  cites: 0
  citedby: 0
  pages: "391-402"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Chlipala13"
- title: "Formal Verification of Hardware Synthesis"
  author:
  - name: "Thomas Braibant"
    link: "https://researchr.org/alias/thomas-braibant"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-39799-8_14"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-39799-8_14"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cav/BraibantC13"
  researchr: "https://researchr.org/publication/BraibantC13"
  cites: 0
  citedby: 0
  pages: "213-228"
  booktitle: "cav"
  kind: "inproceedings"
  key: "BraibantC13"
- title: "Invited talk: the blast query language for software verification"
  author:
  - name: "Dirk Beyer"
    link: "https://researchr.org/alias/dirk-beyer"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Thomas A. Henzinger"
    link: "https://researchr.org/alias/thomas-a.-henzinger"
  - name: "Ranjit Jhala"
    link: "https://researchr.org/alias/ranjit-jhala"
  - name: "Rupak Majumdar"
    link: "https://researchr.org/alias/rupak-majumdar"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/1013963.1013964"
  links:
    doi: "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: "ppdp"
  kind: "inproceedings"
  key: "BeyerCHJM04:0"
- title: "Mostly-automated verification of low-level programs in computational separation logic"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/1993498.1993526"
  links:
    doi: "http://doi.acm.org/10.1145/1993498.1993526"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/Chlipala11"
  researchr: "https://researchr.org/publication/Chlipala11"
  cites: 0
  citedby: 0
  pages: "234-245"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "Chlipala11"
- title: "Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2010"
  doi: "http://www.usenix.org/events/osdi10/tech/full_papers/Chlipala.pdf"
  links:
    doi: "http://www.usenix.org/events/osdi10/tech/full_papers/Chlipala.pdf"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/osdi/Chlipala10"
  researchr: "https://researchr.org/publication/Chlipala10-1"
  cites: 0
  citedby: 0
  pages: "105-118"
  booktitle: "osdi"
  kind: "inproceedings"
  key: "Chlipala10-1"
- title: "A certified type-preserving compiler from lambda calculus to assembly language"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1250734.1250742"
  links:
    doi: "http://doi.acm.org/10.1145/1250734.1250742"
  tags:
  - "compiler"
  researchr: "https://researchr.org/publication/Chlipala07"
  cites: 0
  citedby: 0
  pages: "54-65"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "Chlipala07"
- title: "Type-based verification of assembly language for compiler debugging"
  author:
  - name: "Bor-Yuh Evan Chang"
    link: "https://researchr.org/alias/bor-yuh-evan-chang"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "George C. Necula"
    link: "https://researchr.org/alias/george-c.-necula"
  - name: "Robert R. Schneck"
    link: "https://researchr.org/alias/robert-r.-schneck"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1040294.1040303"
  links:
    doi: "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: "tldi"
  kind: "inproceedings"
  key: "ChangCNS05a"
- title: "Position Paper: Thoughts on Programming with Proof Assistants"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.entcs.2006.10.035"
  links:
    doi: "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: "ENTCS"
  volume: "174"
  number: "7"
  pages: "17-21"
  kind: "article"
  key: "Chlipala07:0"
- title: "Effective interactive proofs for higher-order imperative programs"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "J. Gregory Malecha"
    link: "https://researchr.org/alias/j.-gregory-malecha"
  - name: "Greg Morrisett"
    link: "https://researchr.org/alias/greg-morrisett"
  - name: "Avraham Shinnar"
    link: "https://researchr.org/alias/avraham-shinnar"
  - name: "Ryan Wisnesky"
    link: "https://researchr.org/alias/ryan-wisnesky"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596550.1596565"
  links:
    doi: "http://doi.acm.org/10.1145/1596550.1596565"
  researchr: "https://researchr.org/publication/ChlipalaMMSW09"
  cites: 0
  citedby: 0
  pages: "79-90"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "ChlipalaMMSW09"
- title: "Experience Implementing a Performant Category-Theory Library in Coq"
  author:
  - name: "Jason Gross"
    link: "https://researchr.org/alias/jason-gross"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "David I. Spivak"
    link: "https://researchr.org/alias/david-i.-spivak"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_18"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_18"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/GrossCS14"
  researchr: "https://researchr.org/publication/GrossCS14"
  cites: 0
  citedby: 0
  pages: "275-291"
  booktitle: "itp"
  kind: "inproceedings"
  key: "GrossCS14"
- title: "A verified compiler for an impure functional language"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1706299.1706312"
  abstract: "We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to big-step operational semantics for the source and target languages. Compilation is staged and includes standard phases like translation to continuation-passing style and closure conversion, as well as a common subexpression elimination optimization. In this work, our focus has been on discovering and using techniques that make our proofs easy to engineer and maintain. While most programming language work with proof assistants uses very manual proof styles, all of our proofs are implemented as adaptive programs in Coq's tactic language, making it possible to reuse proofs unchanged as new language features are added. In this paper, we focus especially on phases of compilation that rearrange the structure of syntax with nested variable binders. That aspect has been a key challenge area in past compiler verification projects, with much more effort expended in the statement and proof of binder-related lemmas than is found in standard pencil-and-paper proofs. We show how to exploit the representation technique of parametric higher-order abstract syntax to avoid the need to prove any of the usual lemmas about binder manipulation, often leading to proofs that are actually shorter than their pencil-and-paper analogues. Our strategy is based on a new approach to encoding operational semantics which delegates all concerns about substitution to the meta language, without using features incompatible with general-purpose type theories like Coq's logic."
  links:
    doi: "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: "POPL"
  kind: "inproceedings"
  key: "Chlipala10"
- title: "Ur: statically-typed metaprogramming with type-level record computation"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1806596.1806612"
  links:
    doi: "http://doi.acm.org/10.1145/1806596.1806612"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/Chlipala10"
  researchr: "https://researchr.org/publication/Chlipala10-0"
  cites: 0
  citedby: 1
  pages: "122-133"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "Chlipala10-0"
- title: "Parametric higher-order abstract syntax for mechanized semantics"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1411204.1411226"
  links:
    doi: "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: "ICFP"
  kind: "inproceedings"
  key: "Chlipala08"
- title: "Strict bidirectional type checking"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Leaf Petersen"
    link: "https://researchr.org/alias/leaf-petersen"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1040294.1040301"
  links:
    doi: "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: "tldi"
  kind: "inproceedings"
  key: "ChlipalaPH05"
- title: "An Introduction to Programming and Proving with Dependent Types in Coq"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2010"
  doi: "http://dx.doi.org/10.6092/issn.1972-5787/1978"
  links:
    doi: "http://dx.doi.org/10.6092/issn.1972-5787/1978"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfrea/Chlipala10"
  researchr: "https://researchr.org/publication/Chlipala10-2"
  cites: 0
  citedby: 0
  journal: "jfrea"
  volume: "3"
  number: "2"
  pages: "1-93"
  kind: "article"
  key: "Chlipala10-2"
- title: "Generating Tests from Counterexamples"
  author:
  - name: "Dirk Beyer"
    link: "https://researchr.org/alias/dirk-beyer"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Thomas A. Henzinger"
    link: "https://researchr.org/alias/thomas-a.-henzinger"
  - name: "Ranjit Jhala"
    link: "https://researchr.org/alias/ranjit-jhala"
  - name: "Rupak Majumdar"
    link: "https://researchr.org/alias/rupak-majumdar"
  year: "2004"
  doi: "http://csdl.computer.org/comp/proceedings/icse/2004/2163/00/21630326abs.htm"
  links:
    doi: "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: "ICSE"
  kind: "inproceedings"
  key: "BeyerCM04"
- title: "Invited talk: the blast query language for software verification"
  author:
  - name: "Dirk Beyer"
    link: "https://researchr.org/alias/dirk-beyer"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Thomas A. Henzinger"
    link: "https://researchr.org/alias/thomas-a.-henzinger"
  - name: "Ranjit Jhala"
    link: "https://researchr.org/alias/ranjit-jhala"
  - name: "Rupak Majumdar"
    link: "https://researchr.org/alias/rupak-majumdar"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/1014007.1014028"
  links:
    doi: "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: "PEPM"
  kind: "inproceedings"
  key: "BeyerCHJM04"
- title: "Modular development of certified program verifiers with a proof assistant, "
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2008"
  doi: "http://dx.doi.org/10.1017/S0956796808006904"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796808006904"
  tags:
  - "proof assistant"
  - "program verification"
  researchr: "https://researchr.org/publication/Chlipala08%3A0"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "18"
  number: "5-6"
  pages: "599-647"
  kind: "article"
  key: "Chlipala08:0"
- title: "Modular development of certified program verifiers with a proof assistant"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1159803.1159825"
  links:
    doi: "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: "ICFP"
  kind: "inproceedings"
  key: "Chlipala06"
- title: "The Blast Query Language for Software Verification."
  author:
  - name: "Dirk Beyer"
    link: "https://researchr.org/alias/dirk-beyer"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Thomas A. Henzinger"
    link: "https://researchr.org/alias/thomas-a.-henzinger"
  - name: "Ranjit Jhala"
    link: "https://researchr.org/alias/ranjit-jhala"
  - name: "Rupak Majumdar"
    link: "https://researchr.org/alias/rupak-majumdar"
  year: "2004"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3148&spage=2"
  links:
    doi: "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: "SAS"
  kind: "inproceedings"
  key: "BeyerCHJM04:1"
- title: "A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety"
  author:
  - name: "Bor-Yuh Evan Chang"
    link: "https://researchr.org/alias/bor-yuh-evan-chang"
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "George C. Necula"
    link: "https://researchr.org/alias/george-c.-necula"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/11609773_12"
  links:
    doi: "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: "vmcai"
  kind: "inproceedings"
  key: "ChangCN06"