publications:
- title: "Quotienting the delay monad by weak bisimilarity"
  author:
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2019"
  doi: "https://doi.org/10.1017/S0960129517000184"
  links:
    doi: "https://doi.org/10.1017/S0960129517000184"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/ChapmanUV19"
  researchr: "https://researchr.org/publication/ChapmanUV19"
  cites: 0
  citedby: 0
  journal: "mscs"
  volume: "29"
  number: "1"
  pages: "67-92"
  kind: "article"
  key: "ChapmanUV19"
- title: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "Robert Atkey"
    link: "https://researchr.org/alias/robert-atkey"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2018"
  doi: "https://doi.org/10.1145/3236785"
  links:
    doi: "https://doi.org/10.1145/3236785"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AllaisA0MM18"
  researchr: "https://researchr.org/publication/AllaisA0MM18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "AllaisA0MM18"
- title: "Type-and-scope safe programs and their proofs"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3018610.3018613"
  links:
    doi: "http://doi.acm.org/10.1145/3018610.3018613"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Allais0MM17"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/Allais0MM17"
  cites: 0
  citedby: 0
  pages: "195-207"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "Allais0MM17"
- title: "Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Orestis Melkonian"
    link: "https://researchr.org/alias/orestis-melkonian"
  - name: "Lucas Escot"
    link: "https://researchr.org/alias/lucas-escot"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/ulf-norell"
  year: "2022"
  doi: "https://doi.org/10.1145/3546189.3549920"
  links:
    doi: "https://doi.org/10.1145/3546189.3549920"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/CockxME0N22"
  researchr: "https://researchr.org/publication/CockxME0N22"
  cites: 0
  citedby: 0
  pages: "108-122"
  booktitle: "haskell"
  kind: "inproceedings"
  key: "CockxME0N22"
- title: "Formalizing Restriction Categories"
  author:
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2017"
  doi: "https://doi.org/10.6092/issn.1972-5787/6237"
  links:
    doi: "https://doi.org/10.6092/issn.1972-5787/6237"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfrea/ChapmanUV17"
  researchr: "https://researchr.org/publication/ChapmanUV17"
  cites: 0
  citedby: 0
  journal: "jfrea"
  volume: "10"
  number: "1"
  pages: "1-36"
  kind: "article"
  key: "ChapmanUV17"