bib.bib

@article{Mohri02,
  author = {Mohri, Mehryar},
  title = {{Semiring Frameworks and Algorithms for Shortest-distance Problems}},
  journal = {J. Autom. Lang. Comb.},
  issue_date = {January 2002},
  volume = {7},
  number = {3},
  month = jan,
  year = {2002},
  issn = {1430-189X},
  pages = {321--350},
  numpages = {30},
  url = {http://dl.acm.org/citation.cfm?id=639508.639512},
  acmid = {639512},
  publisher = {Otto-von-Guericke-Universitat},
  address = {Magdeburg, Germany, Germany},
  keywords = {finite automata, rational power series, semirings, shortest-paths algorithms},
}

@misc{Norell07,
  author = {Ulf Norell},
  title = {{Towards a practical programming language based on dependent type theory}},
  year = {2007}
}

@misc{stdlib,
  author = {Nils Anders Danielsson et al.},
  title = {{The Agda Standard Library}},
  year = {2007},
  note = {https://github.com/agda/agda-stdlib}
}

@article {4-colour,
  author = {Gonthier, Georges},
  title = {{Formal proof---the four-color theorem}},
  journal = {Notices Amer. Math. Soc.},
  fjournal = {Notices of the American Mathematical Society},
  volume = {55},
  year = {2008},
  number = {11},
  pages = {1382--1393},
  issn = {0002-9920},
  coden = {AMNOAN},
  mrclass = {05C15 (68T15)},
  mrnumber = {2463991},
  mrreviewer = {Solomon Marcus},
}

@inproceedings{DBLP:conf/aisc/2008,
  booktitle = {{Intelligent Computer Mathematics, 9th International Conference, {AISC}
    2008, 15th Symposium, Calculemus 2008, 7th International Conference,
      {MKM} 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings}},
  editor = {Serge Autexier and
    John A. Campbell and
      Julio Rubio and
      Volker Sorge and
      Masakazu Suzuki and
      Freek Wiedijk},
  title = {{On Correctness of Mathematical Texts}},
  series = {Lecture Notes in Computer Science},
  volume = {5144},
  publisher = {Springer},
  year = {2008},
  isbn = {978-3-540-85109-7},
  timestamp = {Tue, 03 Jul 2012 20:30:28 +0200},
  biburl = {http://dblp2.uni-trier.de/rec/bib/conf/aisc/2008},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  pages = {585}
}

@inbook{Naumowicz2009,
  author = {{Naumowicz, Adam and Korni{\l}owicz, Artur}},
  editor = {Berghofer, Stefan
    and Nipkow, Tobias
    and Urban, Christian
    and Wenzel, Makarius},
  title = {{A Brief Overview of Mizar}},
  booktitle = {{Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}},
  year = {2009},
  publisher = {Springer Berlin Heidelberg},
  address = {Berlin, Heidelberg},
  pages = {67--72},
  isbn = {978-3-642-03359-9},
  doi = {10.1007/978-3-642-03359-9_5},
  url = {http://dx.doi.org/10.1007/978-3-642-03359-9_5}
}

@book{curry1980h,
  title = {{To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism}},
  author = {Curry, H.B. and Hindley, J.R. and Seldin, J.P.},
  isbn = {9780123490506},
  lccn = {lc80040139},
  url = {https://books.google.co.uk/books?id = r0SRQAAACAAJ},
  year = {1980},
  publisher = {Academic Press}
}

@article{Leroy-Compcert-CACM,
  author = {Xavier Leroy},
  title = {{Formal verification of a realistic compiler}},
  journal = {Communications of the ACM},
  year = 2009,
  volume = 52,
  number = 7,
  pages = {107--115},
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
  pubkind = {journal-int-mono},
  abstract = {This paper reports on the development and formal verification (proof
of semantic preservation) of CompCert, a compiler from Clight (a
large subset of the C programming language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its correctness.  Such a verified compiler is useful in
the context of critical software and its formal verification: the
verification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as
well.}
}

@ARTICLE{hales-kepler,
  author =
    {Thomas C. Hales and
    Mark Adams and
    Gertrud Bauer and
    Dat Tat Dang and
    John Harrison and
    Truong Le Hoang and
    Cezary Kaliszyk and
    Victor Magron and
    Sean McLaughlin and
    Thang Tat Nguyen and
    Truong Quang Nguyen and
    Tobias Nipkow and
    Steven Obua and
    Joseph Pleso and
    Jason Rute and
    Alexey Solovyev and
    An Hoai Thi Ta and
    Trung Nam Tran and
    Diep Thi Trieu and
    Josef Urban and
    Ky Khac Vu and
    Roland Zumkeller},
  title = {{A formal proof of the Kepler conjecture}},
  journal = {arXiv},
  volume = {1501.02155},
  year = 2015
}

@article{CakeML,
 author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
 title = {{CakeML: A Verified Implementation of ML}},
 journal = {SIGPLAN Not.},
 issue_date = {January 2014},
 volume = {49},
 number = {1},
 month = jan,
 year = {2014},
 issn = {0362-1340},
 pages = {179--191},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2578855.2535841},
 doi = {10.1145/2578855.2535841},
 acmid = {2535841},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
}

@book{ahl74,
  author = {Aho, Alfred V. and Hopcroft, John E.},
  title = {{The  Design and Analysis of Computer Algorithms}},
  year = {1974},
  isbn = {0201000296},
  edition = {1st},
  publisher = {Addison-Wesley Longman Publishing Co., Inc.},
  address = {Boston, MA, USA},
}

@techreport{martin-lof:aitot,
  author = {Martin-L\"{o}f, P.},
  citeulike-article-id = {3401321},
  institution = {University of Stockholm},
  keywords = {type-theory},
  posted-at = {2008-10-13 16:23:56},
  priority = {0},
  title = {{An Intuitionistic Theory of Types}},
  year = {1972}
}

@misc{CoqProofAssistant,
  title = {{The Coq Proof Assistant}},
  key = {Coq},
  note = {\url{http://coq.inria.fr/}}
}

@Inbook{Hurkens1995,
  author="Hurkens, Antonius J. C.",
  editor="Dezani-Ciancaglini, Mariangiola
    and Plotkin, Gordon",
  title="A simplification of Girard's paradox",
  bookTitle="Typed Lambda Calculi and Applications: Second International Conference on Typed Lambda Calculi and Applications, TLCA '95 Edinburgh, United Kingdom, April 10--12, 1995 Proceedings",
  year="1995",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="266--278",
  isbn="978-3-540-49178-1",
  doi="10.1007/BFb0014058",
  url="http://dx.doi.org/10.1007/BFb0014058"
}

@inbook{howard:tfatnoc,
  address = {London-New York},
  author = {Howard, W. A.},
  booktitle = {To H. B. Curry: essays on combinatory logic, lambda calculus and formalism},
  citeulike-article-id = {3506102},
  editor = {Seldin, J. P. and Hindley, J. R.},
  keywords = {type-theory},
  pages = {480--490},
  posted-at = {2008-11-12 14:35:50},
  priority = {2},
  publisher = {Academic Press},
  title = {{The formulae-as-types notion of construction}},
  year = {1980}
}

@misc{Griffin12,
  author = {Griffin, T. G.},
  institution = {University of Cambridge},
  howpublished = {\url{http://dimacs.rutgers.edu/Workshops/NetworkServices/Slides/Tim_Griffin.pdf}},
  year = {2012},
  title = {{Algebraic Path Finding}}
}

@Article{Dijkstra1959,
  author="Dijkstra, E. W.",
  title="A note on two problems in connexion with graphs",
  journal="Numerische Mathematik",
  year="1959",
  volume="1",
  number="1",
  pages="269--271",
  issn="0945-3245",
  doi="10.1007/BF01386390",
  url="http://dx.doi.org/10.1007/BF01386390"
}

@book{Milner1990,
  author = {Milner, Robin and Tofte, Mads and Harper, Robert},
  title = {The Definition of Standard ML},
  year = {1990},
  isbn = {0-262-63132-6},
  publisher = {MIT Press},
  address = {Cambridge, MA, USA},
}

@article{ocaml,
  author = {Leroy, Xavier},
  citeulike-article-id = {13114320},
  howpublished = {\\url{http://caml. inria. fr/ocaml/index. en. html}},
  keywords = {ocaml},
  posted-at = {2014-03-22 18:06:28},
  priority = {2},
  title = {{The OCaml programming language}},
  year = {1998}
}

@misc{Haskell2010,
  author = {Simon Marlow},
  title = {{Haskell 2010 Language Report}},
  year = {2010},
  howpublished = {https://www.haskell.org/onlinereport/haskell2010/}
}

INPROCEEDINGS{Griffin10,
  author = {Timothy G. Griffin},
  title = {The stratified shortest paths problem (invited paper)},
  booktitle = {in Proc. of COMSNETS},
  year = {2010}
}

@inproceedings{Griffin10,
  author = {Griffin, Timothy G.},
  title = {The Stratified Shortest-paths Problem},
  booktitle = {Proceedings of the 2Nd International Conference on COMmunication Systems and NETworks},
  series = {COMSNETS'10},
  year = {2010},
  isbn = {978-1-4244-5487-7},
  location = {Bangalore, India},
  pages = {268--277},
  numpages = {10},
  url = {http://dl.acm.org/citation.cfm?id=1831443.1831472},
  acmid = {1831472},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
}

@article{Barthe03,
  author = {Barthe, Gilles and Capretta, Venanzio and Pons, Olivier},
  title = {Setoids in Type Theory},
  journal = {J. Funct. Program.},
  issue_date = {March 2003},
  volume = {13},
  number = {2},
  month = mar,
  year = {2003},
  issn = {0956-7968},
  pages = {261--293},
  numpages = {33},
  url = {http://dx.doi.org/10.1017/S0956796802004501},
  doi = {10.1017/S0956796802004501},
  acmid = {967854},
  publisher = {Cambridge University Press},
  address = {New York, NY, USA},
}

@Inbook{Droste2009,
  author="Droste, Manfred
    and Kuich, Werner",
  editor="Droste, Manfred
    and Kuich, Werner
    and Vogler, Heiko",
  title="Semirings and Formal Power Series",
  bookTitle="Handbook of Weighted Automata",
  year="2009",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="3--28",
  isbn="978-3-642-01492-5",
  doi="10.1007/978-3-642-01492-5_1",
  url="http://dx.doi.org/10.1007/978-3-642-01492-5_1"
}

@MISC{Abel98,
  author = {Andreas Abel},
  title = {foetus --- Termination Checker for Simple Functional Programs},
  year = {1998}
}

@misc{stack,
  author = {Commercial Haskell SIG},
  title = {{The Haskell Tool Stack}},
  year = {2015},
  note = {https://docs.haskellstack.org/en/stable/README/}
}

@inproceedings{ghc,
 author = {Hall, Cordelia V. and Hammond, Kevin and Partain, Will and Peyton Jones, Simon L. and Wadler, Philip},
 title = {The Glasgow Haskell Compiler: A Retrospective},
 booktitle = {Proceedings of the 1992 Glasgow Workshop on Functional Programming},
 year = {1993},
 isbn = {3-540-19820-2},
 pages = {62--71},
 numpages = {10},
 url = {http://dl.acm.org/citation.cfm?id=647557.729914},
 acmid = {729914},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
}

@misc{git,
  title = {{Git version control system}},
  note = {https://git-scm.com/}
}