@inproceedings{McBride04,
  title = {Epigram: Practical Programming with Dependent Types},
  author = {Conor McBride},
  year = {2004},
  doi = {10.1007/11546382_3},
  url = {http://dx.doi.org/10.1007/11546382_3},
  tags = {Intrinsic-Verification, programming},
  researchr = {https://researchr.org/publication/McBride04},
  cites = {0},
  citedby = {0},
  pages = {130-170},
  booktitle = {Advanced Functional Programming, 5th International School, AFP 2004, Tartu, Estonia, August 14-21, 2004, Revised Lectures},
  editor = {Varmo Vene and Tarmo Uustalu},
  volume = {3622},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-28540-7},
}

@inproceedings{McBrideM04-0,
  title = {Functional pearl: I am not a number-I am a free variable},
  author = {Conor McBride and James McKinna},
  year = {2004},
  doi = {10.1145/1017472.1017477},
  url = {http://doi.acm.org/10.1145/1017472.1017477},
  researchr = {https://researchr.org/publication/McBrideM04-0},
  cites = {0},
  citedby = {0},
  pages = {1-9},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004},
  editor = {Henrik Nilsson},
  publisher = {ACM},
}

@inproceedings{McBride08:0,
  title = {Clowns to the left of me, jokers to the right (pearl): dissecting data structures},
  author = {Conor McBride},
  year = {2008},
  doi = {10.1145/1328438.1328474},
  url = {http://doi.acm.org/10.1145/1328438.1328474},
  tags = {data-flow},
  researchr = {https://researchr.org/publication/McBride08%3A0},
  cites = {0},
  citedby = {0},
  pages = {287-295},
  booktitle = {Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008},
  editor = {George C. Necula and Philip Wadler},
  publisher = {ACM},
  isbn = {978-1-59593-689-9},
}

@inproceedings{ChapmanDMM10,
  title = {The gentle art of levitation},
  author = {James Chapman and Pierre-Évariste Dagand and Conor McBride and Peter Morris},
  year = {2010},
  doi = {10.1145/1863543.1863547},
  url = {http://doi.acm.org/10.1145/1863543.1863547},
  researchr = {https://researchr.org/publication/ChapmanDMM10},
  cites = {0},
  citedby = {0},
  pages = {3-14},
  booktitle = {Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010},
  editor = {Paul Hudak and Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-60558-794-3},
}

@article{McBrideM04,
  title = {The view from the left},
  author = {Conor McBride and James McKinna},
  year = {2004},
  doi = {10.1017/S0956796803004829},
  url = {http://dx.doi.org/10.1017/S0956796803004829},
  researchr = {https://researchr.org/publication/McBrideM04},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {14},
  number = {1},
  pages = {69-111},
}

@inproceedings{McBrideGM04,
  title = {A Few Constructions on Constructors},
  author = {Conor McBride and Healfdene Goguen and James McKinna},
  year = {2004},
  doi = {10.1007/11617990_12},
  url = {http://dx.doi.org/10.1007/11617990_12},
  researchr = {https://researchr.org/publication/McBrideGM04},
  cites = {0},
  citedby = {0},
  pages = {186-200},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers},
  editor = {Jean-Christophe Filliâtre and Christine Paulin-Mohring and Benjamin Werner},
  volume = {3839},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-31428-8},
}

@inproceedings{McBride09,
  title = {Let s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)},
  author = {Conor McBride},
  year = {2009},
  doi = {10.1007/978-3-642-03741-2_9},
  url = {http://dx.doi.org/10.1007/978-3-642-03741-2_9},
  researchr = {https://researchr.org/publication/McBride09},
  cites = {0},
  citedby = {0},
  pages = {113-126},
  booktitle = {Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings},
  editor = {Alexander Kurz and Marina Lenisa and Andrzej Tarlecki},
  volume = {5728},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-03740-5},
}

@inproceedings{AbbottAGM03,
  title = {Derivatives of Containers},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride},
  year = {2003},
  url = {http://link.springer.de/link/service/series/0558/bibs/2701/27010016.htm},
  researchr = {https://researchr.org/publication/AbbottAGM03},
  cites = {0},
  citedby = {0},
  pages = {16-30},
  booktitle = {Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings},
  editor = {Martin Hofmann},
  volume = {2701},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-40332-9},
}

@article{AllaisA0MM18,
  title = {A type and scope safe universe of syntaxes with binding: their semantics and proofs},
  author = {Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna},
  year = {2018},
  doi = {10.1145/3236785},
  url = {https://doi.org/10.1145/3236785},
  researchr = {https://researchr.org/publication/AllaisA0MM18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
}

@inproceedings{GoguenMM06,
  title = {Eliminating Dependent Pattern Matching},
  author = {Healfdene Goguen and Conor McBride and James McKinna},
  year = {2006},
  doi = {10.1007/11780274_27},
  url = {http://dx.doi.org/10.1007/11780274_27},
  tags = {pattern matching},
  researchr = {https://researchr.org/publication/GoguenMM06},
  cites = {0},
  citedby = {0},
  pages = {521-540},
  booktitle = {Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday},
  editor = {Kokichi Futatsugi and Jean-Pierre Jouannaud and José Meseguer},
  volume = {4060},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-35462-X},
}

@inproceedings{BradyMM03,
  title = {Inductive Families Need Not Store Their Indices},
  author = {Edwin Brady and Conor McBride and James McKinna},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=115},
  researchr = {https://researchr.org/publication/BradyMM03},
  cites = {0},
  citedby = {0},
  pages = {115-129},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
  editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  volume = {3085},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22164-6},
}

@article{AbbottAMG05,
  title = {for Data: Differentiating Data Structures},
  author = {Michael Abbott and Thorsten Altenkirch and Conor McBride and Neil Ghani},
  year = {2005},
  url = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=65&issue=1&spage=1},
  tags = {data-flow},
  researchr = {https://researchr.org/publication/AbbottAMG05},
  cites = {0},
  citedby = {0},
  journal = {Fundamenta Informaticae},
  volume = {65},
  number = {1-2},
  pages = {1-28},
}

@inproceedings{ChapmanAM05,
  title = {Epigram reloaded: a standalone typechecker for ETT},
  author = {James Chapman and Thorsten Altenkirch and Conor McBride},
  year = {2005},
  researchr = {https://researchr.org/publication/ChapmanAM05},
  cites = {0},
  citedby = {0},
  pages = {79-94},
  booktitle = {Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005},
  editor = {Marko C. J. D. van Eekelen},
  volume = {6},
  series = {Trends in Functional Programming},
  publisher = {Intellect},
  isbn = {978-1-84150-176-5},
}

@article{McBride2018,
  title = {Everybody's Got To Be Somewhere},
  author = {Conor McBride},
  year = {2018},
  month = {Jul},
  doi = {10.4204/eptcs.275.6},
  url = {http://dx.doi.org/10.4204/EPTCS.275.6},
  researchr = {https://researchr.org/publication/McBride2018},
  cites = {0},
  citedby = {0},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {275},
  pages = {53-69},
}

@inproceedings{AltenkirchM02,
  title = {Generic Programming within Dependently Typed Programming},
  author = {Thorsten Altenkirch and Conor McBride},
  year = {2002},
  tags = {generic programming, programming},
  researchr = {https://researchr.org/publication/AltenkirchM02},
  cites = {0},
  citedby = {0},
  pages = {1-20},
  booktitle = {Generic Programming, IFIP TC2/WG2.1 Working Conference on Generic Programming, July 11-12, 2002, Dagstuhl, Germany},
  editor = {Jeremy Gibbons and Johan  Jeuring},
  volume = {243},
  series = {IFIP Conference Proceedings},
  publisher = {Kluwer},
  isbn = {1-4020-7374-7},
}

@article{LohMS10,
  title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus},
  author = {Andres Löh and Conor McBride and Wouter Swierstra},
  year = {2010},
  doi = {10.3233/FI-2010-304},
  url = {http://dx.doi.org/10.3233/FI-2010-304},
  researchr = {https://researchr.org/publication/LohMS10},
  cites = {0},
  citedby = {0},
  journal = {Fundamenta Informaticae},
  volume = {102},
  number = {2},
  pages = {177-207},
}

@inproceedings{MorrisAM04,
  title = {Exploring the Regular Tree Types},
  author = {Peter Morris and Thorsten Altenkirch and Conor McBride},
  year = {2004},
  doi = {10.1007/11617990_16},
  url = {http://dx.doi.org/10.1007/11617990_16},
  researchr = {https://researchr.org/publication/MorrisAM04},
  cites = {0},
  citedby = {0},
  pages = {252-267},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers},
  editor = {Jean-Christophe Filliâtre and Christine Paulin-Mohring and Benjamin Werner},
  volume = {3839},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-31428-8},
}

@article{McbrideP08,
  title = {Applicative programming with effects},
  author = {Conor McBride and Ross Paterson},
  year = {2008},
  doi = {10.1017/S0956796807006326},
  url = {http://dx.doi.org/10.1017/S0956796807006326},
  tags = {programming},
  researchr = {https://researchr.org/publication/McbrideP08},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {18},
  number = {1},
  pages = {1-13},
}

@inproceedings{McBride07,
  title = {What s the deal with dependent types?},
  author = {Conor McBride},
  year = {2007},
  doi = {10.1145/1190315.1190316},
  url = {http://doi.acm.org/10.1145/1190315.1190316},
  researchr = {https://researchr.org/publication/McBride07},
  cites = {0},
  citedby = {0},
  pages = {1-2},
  booktitle = {Proceedings of TLDI 07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007},
  editor = {François Pottier and George C. Necula},
  publisher = {ACM},
  isbn = {1-59593-393-X},
}

@inproceedings{AbbottAGM04,
  title = {Constructing Polymorphic Programs with Quotient Types},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3125&spage=2},
  researchr = {https://researchr.org/publication/AbbottAGM04},
  cites = {0},
  citedby = {0},
  pages = {2-15},
  booktitle = {Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings},
  editor = {Dexter Kozen and Carron Shankland},
  volume = {3125},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22380-0},
}

@article{McBride02,
  title = {Faking it: Simulating dependent types in Haskell},
  author = {Conor McBride},
  year = {2002},
  tags = {Haskell},
  researchr = {https://researchr.org/publication/McBride02},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {12},
  number = {4&5},
  pages = {375-392},
}

@inproceedings{PrinceGM08,
  title = {Proving Properties about Lists Using Containers},
  author = {Rawle Prince and Neil Ghani and Conor McBride},
  year = {2008},
  doi = {10.1007/978-3-540-78969-7_9},
  url = {http://dx.doi.org/10.1007/978-3-540-78969-7_9},
  researchr = {https://researchr.org/publication/PrinceGM08},
  cites = {0},
  citedby = {0},
  pages = {97-112},
  booktitle = {Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings},
  editor = {Jacques Garrigue and Manuel V. Hermenegildo},
  volume = {4989},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-78968-0},
}

@inproceedings{AltenkirchMS07,
  title = {Observational equality, now!},
  author = {Thorsten Altenkirch and Conor McBride and Wouter Swierstra},
  year = {2007},
  doi = {10.1145/1292597.1292608},
  url = {http://doi.acm.org/10.1145/1292597.1292608},
  researchr = {https://researchr.org/publication/AltenkirchMS07},
  cites = {0},
  citedby = {0},
  pages = {57-68},
  booktitle = {Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007},
  editor = {Aaron Stump and Hongwei Xi},
  publisher = {ACM},
  isbn = {978-1-59593-677-6},
}