Previous Up

References

[1]
Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C.7, pages 739–782. North-Holland, Amsterdam, 1977.
[2]
J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, first edition, 307 p. 52 illus. edition, 2011.
[3]
Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers. Cambridge University Press, New York, NY, USA, 2014.
[4]
A. Arnold and I. Guessarian. Mathematics for Computer Science. Prentice-Hall, 1996.
[5]
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[6]
H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.
[7]
H.P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–310. Oxford University Press, New York, 1992.
[8]
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
[9]
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Serie. Springer Verlag, 2004. http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html
[10]
S. Burris and H. Sankappanavar. A Course in Universal Algebra. Springer Verlag, 1981. http://www.cs.uu.nl/people/franka/ref
[11]
Adam Chlipala. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013.
[12]
E.M. Clarke, O. Grumberg, and D Peled. Model Checking. MIT Press, 2000.
[13]
B. A. Davey and H. A. Priestley. Introduction to Lattices and Order: Second Edition. Cambridge University Press, 2002.
[14]
J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988.
[15]
Chris Hankin. Lambda Calculi: A Guide for Computer Scientists, volume 3 of Graduate Texts in Computer Science. Clarendon Press, Oxford, 1994.
[16]
Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, New York, NY, USA, 2012.
[17]
David Makinson. Sets, Logic and Maths for Computing. Springer Publishing Company, Incorporated, 1 edition, 2008.
[18]
John C. Mitchell. Concepts in programming languages. Cambridge University Press, 2003.
[19]
H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
[20]
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2007.
[21]
Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
[22]
Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005.
[23]
Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjoberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2015.
[24]
I. Poernomo, J. Crossley, and M. Wirsing. Adapting Proofs-as-Programs, The Curry–Howard Protocol. Monographs in Computer Science. Springer Verlag, 2005.
[25]
A. S. Troelstra and H. Schwichtenberg. Basic proof theory. Cambridge University Press, New York, NY, USA, 1996.
[26]
D. van Dalen. Logic and Structure. Springer Verlag, Berlin, Germany, 1983.
[27]
G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge, Massachusetts, February 1993.




Enviar comentários e dúvidas para (retire os UUU) : desousaUUU@UUUdi.ubi.pt


Previous Up