@inproceedings{NorellJ04,
  title = {Prototyping Generic Programming in Template Haskell},
  author = {Ulf Norell and Patrik Jansson},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3125&spage=314},
  tags = {generic programming, Haskell, programming},
  researchr = {https://researchr.org/publication/NorellJ04},
  cites = {0},
  citedby = {0},
  pages = {314-333},
  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},
}

@inproceedings{Norell08,
  title = {Dependently Typed Programming in Agda},
  author = {Ulf Norell},
  year = {2008},
  doi = {10.1007/978-3-642-04652-0_5},
  url = {http://dx.doi.org/10.1007/978-3-642-04652-0_5},
  tags = {programming},
  researchr = {https://researchr.org/publication/Norell08},
  cites = {0},
  citedby = {0},
  pages = {230-266},
  booktitle = {Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures},
  editor = {Pieter W. M. Koopman and Rinus Plasmeijer and S. Doaitse Swierstra},
  volume = {5832},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-04651-3},
}

@inproceedings{BoveDN09,
  title = {A Brief Overview of Agda - A Functional Language with Dependent Types},
  author = {Ana Bove and Peter Dybjer and Ulf Norell},
  year = {2009},
  doi = {10.1007/978-3-642-03359-9_6},
  url = {http://dx.doi.org/10.1007/978-3-642-03359-9_6},
  researchr = {https://researchr.org/publication/BoveDN09},
  cites = {0},
  citedby = {0},
  pages = {73-78},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  editor = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
  volume = {5674},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-03358-2},
}

@inproceedings{AbelBBHN05,
  title = {Verifying haskell programs using constructive type theory},
  author = {Andreas Abel and Marcin Benke and Ana Bove and John Hughes and Ulf Norell},
  year = {2005},
  doi = {10.1145/1088348.1088355},
  url = {http://doi.acm.org/10.1145/1088348.1088355},
  tags = {program verification, Haskell, type theory},
  researchr = {https://researchr.org/publication/AbelBBHN05},
  cites = {0},
  citedby = {0},
  pages = {62-73},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2005, Tallinn, Estonia, September 30, 2005},
  editor = {Daan Leijen},
  publisher = {ACM},
  isbn = {1-59593-071-X},
}

@inproceedings{Norell09,
  title = {Dependently typed programming in Agda},
  author = {Ulf Norell},
  year = {2009},
  doi = {10.1145/1481861.1481862},
  url = {http://doi.acm.org/10.1145/1481861.1481862},
  tags = {programming},
  researchr = {https://researchr.org/publication/Norell09},
  cites = {0},
  citedby = {0},
  pages = {1-2},
  booktitle = {Proceedings of TLDI 08: 2008 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009},
  editor = {Andrew Kennedy and Amal Ahmed},
  publisher = {ACM},
  isbn = {978-1-60558-420-1},
}

@inproceedings{NorellJ03,
  title = {Polytypic Programming in Haskell},
  author = {Ulf Norell and Patrik Jansson},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3145&spage=168},
  tags = {polytypic programming, Haskell, programming, polytypic},
  researchr = {https://researchr.org/publication/NorellJ03},
  cites = {0},
  citedby = {0},
  pages = {168-184},
  booktitle = {Implementation of Functional Languages, 15th International Workshop, IFL 2003, Edinburgh, UK, September 8-11, 2003, Revised Papers},
  editor = {Philip W. Trinder and Greg Michaelson and Ricardo Pena},
  volume = {3145},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-23727-5},
}

@inproceedings{AbelCN05,
  title = {Connecting a Logical Framework to a First-Order Logic Prover},
  author = {Andreas Abel and Thierry Coquand and Ulf Norell},
  year = {2005},
  doi = {10.1007/11559306_17},
  url = {http://dx.doi.org/10.1007/11559306_17},
  tags = {logic},
  researchr = {https://researchr.org/publication/AbelCN05},
  cites = {0},
  citedby = {0},
  pages = {285-301},
  booktitle = {Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings},
  editor = {Bernhard Gramlich},
  volume = {3717},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-29051-6},
}