Podstawy języków programowania w systemie Coq

[Pi14]

Software Foundations, Benjamin C. Pierce et al., 2014.

[BC04]	Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, Yves Bertot and Pierre Castéran, Springer, 2004.
[Ch13]	Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant , Adam Chlipala, The MIT Press, 2013.
[Pi02]	Types and Programming Languages, Benjamin C. Pierce, The MIT Press, 2002.

[B92]	Lambda Calculi with Types, Henk Barendregt, Handbook of Logic in Computer Science (vol. 2), Oxford University Press, 1992.
[BC00]	An Introduction to Dependent Type Theory, Gilles Barthe and Thierry Coquand, Proceedings of APPSEM 2000, Caminha, Portugal, 2000, Springer-Verlag.
[NPS90]	Programming in Martin-Löf's Type Theory: An Introduction, Bengt Nordström, Kent Petersson, and Jan M. Smith, Oxford University Press, 1990.
[P93]	Inductive Definitions in the System Coq - Rules and Properties, Christine Paulin-Mohring, Proceedings of TLCA 1992, LNCS 664, Springer-Verlag, 1993.
[SU06]	Lectures on the Curry-Howard Isomorphism, Morten H. Sørensen and Paweł Urzyczyn, Elsevier, 2006.
[T91]	Type Theory and Functional Programming, Simon Thompson, Addison-Wesley, 1991.