Przemebra/praca-magisterska/bibliography.bib

@Misc{UniMath,
    author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
    title = {{UniMath --- a computer-checked library of univalent mathematics}},
    url = {https://github.com/UniMath/UniMath},
    howpublished = {{available} at \url{https://github.com/UniMath/UniMath}}
 }
 
@Book{hottbook,
  author =    {The {Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address =   {Institute for Advanced Study},
  year =      2013}

@misc{agdastdlib,
  author = {Danielsson, N. and Allais, G and Daggit M. and others},
  title = {Agda Standard Library},
  year = {2013},
  url = {https://github.com/agda/agda-stdlib},
  howpublished = {{available} at \url{https://github.com/agda/agda-stdlib}}
}


@misc{natural-numbers-def,
  author = {Wikipedia contributors},
  title = {Liczby naturalne},
  year = {2018},
  url = {https://pl.wikipedia.org/wiki/Liczby_naturalne},
  howpublished = {{available} at \url{https://pl.wikipedia.org/wiki/Liczby_naturalne}}
}


@misc{proof-assistant-wiki,
  author = {Wikipedia contributors},
  title = {System wspomagający dowodzenie twierdzeń},
  year = {2018},
  url = {https://pl.wikipedia.org/wiki/System_wspomagaj\%C4\%85cy_dowodzenie_twierdze\%C5\%84},
  howpublished = {{available} at \url{https://pl.wikipedia.org/wiki/System_wspomagaj\%C4\%85cy_dowodzenie_twierdze\%C5\%84}}
}

@misc{univalent-foundations,
  author = {Wikipedia contributors},
  title = {Univalent Foundations},
  year = {2018},
  url = {https://en.wikipedia.org/wiki/Univalent_foundations},
  howpublished = {{available} at \url{https://en.wikipedia.org/wiki/Univalent_foundations}}
}

@article{analysisofgirard,
author = {Coquand, Thierry},
year = {1999},
month = {10},
title = {An Analysis of Girard's Paradox}
}

% wiki PML
@article{pmlfirst,
author = {Martin-Löf, Per},
title = {An intuitionistic theory of types},
year = {1972}
}

@book{pmlnotes,
author = {Martin-Löf, Per and Sambin, Giovanni},
title = {Intuitionistic type theory},
publisher = {Napoli : Bibliopolis},
year = {1984}
}
% wiki PML
@article{pmlnewest,
author = {Martin-Löf, Per},
title = {Constructive mathematics and computer programming},
year = {1982}
}

@article{lambdapi,
author = {L{\"o}f, Andres and McBrice, Conor and Swiestra, Wouter},
title = {A tutorial implementation of a dependently typed lambda calculus},
journal = {Fundamenta Informaticae XXI (2001) 1001–1031},
year = {2001}
}

@book{algebra,
author = {Mines, Ray and Richman, Fred and Ruitenburg, Wim},
title = {A Course in Constructive Algebra},
publisher = {Springer-Verlag},
year = {1988}
}

@book{russel,
author = {Russell, B.},
title = {The Principles of Mathematics},
publisher = {Cambridge University Press},
year = {1903}
}

@article{agdafoundation,
author = {Norell, Ulf},
year = {2009},
title = {Dependently Typed Programming in Agda},
journal = {TLDI 2009},
doi = {10.1007/978-3-642-04652-0_5}
}

%Comment praca magisterska
@article{magvbh,
author = {Bui, Viet Ha},
title = {Towards Reasoning about State Transformer Monads in Agda},
year = {2009}
}


%Comment ta nie udana praca xD
@article{magfailed,
author = {M\"{o}rtberg, Anders},
title = {Constructive Algebra in Functional Programming and Type Theory},
year = {2010}
}

@article{lean,
author = {de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and  van Doorn, Floris and  von Raumer, Jakob},
title = {The Lean Theorem Prover},
year = {2015}
}

@article{unifiedtypetheory,
author = {Luo, Zhaohui},
title = {Computation and reasoning: a type theory for computer science},
year = {1994},
publisher = {Oxford University Press, Inc.}
}


@misc{agdaslabe,
  author = {Oğuz, Beren},
  title = {Math},
  year = {2017},
  url = {https://github.com/berenoguz/Math},
  howpublished = {{available} at \url{https://github.com/berenoguz/Math}}
}

@misc{agdawiki,
 author = {Agda contributors},
 title = {Agda wiki},
 year = {2018},
 url = {https://wiki.portal.chalmers.se/agda/pmwiki.php}
}

@mist{wikipedia-o-agdzie,
  author = {Wikipedia contributors},
  title = {Agda - wikipedia},
  year = {2019},
  url = {https://en.wikipedia.org/wiki/Agda_(programming_language)}
}

@misc{przemek,
  author = {Karpiel, Wojciech},
  title = {Przemek},
  year = {2018},
  url = {http://student.agh.edu.pl/~wkarpiel/praca-magisterska/przemek.git},
  howpublished = {{available} at \url{http://student.agh.edu.pl/~wkarpiel/praca-magisterska/przemek.git}}
}

@misc{bauertutorial,
author = {Bauer, Andrej},
title = {How to implement dependent type theory},
year = {2012},
url = {http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/},
howpublished = {{available} at \url{http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/}}
}

@misc{coq,
author = {Huet, Gérardand and Coquand, Thierry and  Murthy, Chet and  Barras, Bruno and others},
title = {Coq Proof Assistant},
year = {1989},
url = {https://coq.inria.fr/},
howpublished = {{available} at \url{https://coq.inria.fr/}}
}

@book{ciesielski,
author = {Ciesielski, Krzysztof},
title ={Set Theory for the Working Mathematician},
publisher = {Cabridge University Press},
year = {1997}
}

@book{bishop,
author = {Bishop, Erret},
title = {Foundations of constructive analysis},
publisher ={Ishi Press International},
year = {1967}
}

%n 1969 Howard observes that another, more "high-level" proof system, referred to as natural deduction, can be directly interpreted in its intuitionistic version as a typed variant of the model of computation known as lambda calculus.
@book{howard,
author = {Howard, William A},
title = {Essays on Combinatory Logic, Lambda Calculus and Formalism},
publisher = {Boston, MA: Academic Press},
year = {1980}
}
@InCollection{sep-mathematics-constructive,
	author       =	{Bridges, Douglas and Palmgren, Erik},
	title        =	{Constructive Mathematics},
	booktitle    =	{The Stanford Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{https://plato.stanford.edu/archives/sum2018/entries/mathematics-constructive/}},
	year         =	{2018},
	edition      =	{Summer 2018},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}
@MISC{Abel98foetus,
    author = {Andreas Abel},
    title = {foetus – Termination Checker for Simple Functional Programs },
    year = {1998},
    url = {https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.3494&rank=1},
    oai = {oai:CiteSeerX.psu:10.1.1.44.3494}
}
@MISC{agda-doc,
title = {Agda’s documentation},
author = {Norell Ulf and others},
year = {2005},
url = {https://agda.readthedocs.io}
}

@article{calculus-of-constructions,
author = {Thierry Coquand and Gerard Huet },
doi = {10.1016/0890-5401(88)90005-3},
title = {The calculus of constructions},
year = {1985}
}