Teoria da Computação
(cod.5384)

Departamento de Informática
Universidade da Beira Interior

Ano lectivo 2006/2007

Esta página no formato pdf, no formato ps

1  Novidades

Contents

2  Docentes

Simão Melo de Sousa (regente) - Gabinete 4.3.

3  Objectivos

Existem limites à capacidade de resolução de problemas por um computador, mesmo na hipótese “idealista” de ausência de restrições, que sejam essas o tempo (de execução) ou o espaço (memória). Para delinear esses limites, visaremos:
  1. perceber a capacidade de computação das máquinas, assim como os seus limites teóricos. Precisaremos de definir formalmente o que é e o que não é um programa, um algoritmo, ou mais genericamente o que é um tratamento efectivo;
  2. perceber os conceitos que fundamentam as linguagens de programação. Precisaremos de determinar e estudar formalmente as construções que determinam a expressividade (ou capacidade de computação) das linguagens de programação assim como o comportamento dos programas.

4  Programa

5  Critérios de Avaliação

A avaliação será realizada por exame e avaliação contínua. Listamos a seguir as diferentes componentes da avaliação.

5.1  Componente Ensino/Aprendizagem

5.2  Admissão e Avaliação por Exame

6  Datas Importantes

7  Material Pedagógico

Apontamentos apresentados e disponibilizados nas aulas

Fichas práticas

Por definir.

8  Horário

Tipo de aula Horário Sala
Teórica Quinta-Feira das 16h00 às 18h00 6.02
Práticas Laboratóriais 1 Quarta-Feira das 11h00 às 13h00 6.14
Práticas Laboratóriais 2 Terça-Feira das 11h00 às 13h00 6.14
Práticas Laboratóriais 3 Terça-Feira das 16h00 às 18h00 6.14
Práticas Laboratóriais 4 Quinta-Feira das 14h00 às 16h00 6.14

9  Atendimento

Horário
Terça-Feira das 14h00 às 16h00

10  Alunos de Engenharia Informática inscritos

Por definir

11  Bibliografia Principal

As referencias principais são: [2, 30, 8, 23, 37]

12  Links úteis

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]
A. Arnold and I. Guessarian. Mathematics for Computer Science. Prentice-Hall, 1996.

[3]
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[4]
D. Bagley. The great computer language shootout. http://www.bagley.org/~doug/shootout

[5]
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.

[6]
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.

[7]
S. Burris and H. Sankappanavar. A Course in Universal Algebra. Springer Verlag, 1981. http://www.cs.uu.nl/people/franka/ref

[8]
E. Chailloux, P. Manoury, and B. Pagano. Developing applications with objective caml. http://caml.inria.fr/oreilly-book, 2003.

[9]
T. Coquand and P. Dybjer. Inductive definitions and type theory: an introduction. In Foundations of Software Technology and Theoretical Computer Science, pages 60–76, 1994. http://www.math.chalmers.se/~peterd/papers/ESSLLI94.ps.gz

[10]
R. Cori and D. Lascar. Mathematical Logic : A course with exercises – Part I. Oxford University Press, 2000.

[11]
R. Cori and D. Lascar. Mathematical Logic : A course with exercises – Part II. Oxford University Press, 2001.

[12]
G. Cousineau and M. Mauny. The functional approach to programming. Cambridge University Press, 1998.

[13]
N. J. Cutland. Computability. Cambridge University Press, 1980.

[14]
B. A. Davey and H. A. Priestley. Introduction to Lattices and Order: Second Edition. Cambridge University Press, 2002.

[15]
G. Dowek. La logique. Coll. Dominos. Flammarion, 1995.

[16]
G. Dowek. Le langage mathématique et les langages de programmation. Voir, entendre, raisonner, calculer. Cité des sciences et de l'industrie, La Villette, Paris, 1997. http://www.lix.polytechnique.fr/~dowek/Vulg/langagelangages.ps.gz

[17]
G. Dowek. Higher-order unification and matching. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 16, pages 1009–1062. Elsevier Science Publishers B.V., 2001.

[18]
G. Dowek. Théories des types. DEA Programmation, Paris VII, 2002. http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz

[19]
P. Fejer and D. Simovici. Mathematical Foundations of Computer Science, Volume 1: Sets, Relations and Induction,. Texts and Monographs in Computer Science. Springer Verlag, 1991.

[20]
E. Gimenez. A tutorial on recursive types in Coq. http://coq.inria.fr/doc-eng.html

[21]
J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988.

[22]
C. Hall and J. O'Donnell. Discrete Mathematics Using A Computer. Springer Verlag, 2000.

[23]
Chris Hankin. Lambda Calculi: A Guide for Computer Scientists, volume 3 of Graduate Texts in Computer Science. Clarendon Press, Oxford, 1994.

[24]
D. R. Hofstadter. Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books, New York, 1979.

[25]
G. Huet. Constructive computation theory. Course Notes, DEA Informatique Université Bordeaux I, October 1992. http://pauillac.inria.fr/~huet/CCT/

[26]
N. D. Jones. Computability and Complexity from a Programming Perspective. Foundations of Computing. MIT Press, Boston, London, 1 edition, 1997.

[27]
J. W. Klop. Term rewriting systems. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, New York, 1992.

[28]
W. Kneale and M. Kneale. O Desenvolvimento da Lógica. Fundação Calouste Gulbenkian, (1962) - 1991. Terceira Edição.

[29]
J. L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood, 1993.

[30]
P. Linz. An introduction to formal languages and automata. Jones and Bartlett Publisher, 2006.

[31]
H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons, Chichester, 1993. http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

[32]
L. Pequet. Programmation fonctionelle - introduction illustrée en objective caml. http://www-rocq.inria.fr/~pecquet/pro/teach/teach.html, 2002.

[33]
A. Pitts. Lecture notes on denotational semantics. University of Cambridge Computer Laboratory, 1999. http://www.cl.cam.ac.uk/Teaching/1998/DenoSema/dens.ps.gz

[34]
A. Pitts. Lecture notes on computation theory. University of Cambridge Computer Laboratory, 2002. http://www.cl.cam.ac.uk/Teaching/2002/CompTheory

[35]
F. Prost and G. Kahn. Checking mathematical facts with coq: Various examples of Coq proofs. http://coq.inria.fr/contribs-eng.html

[36]
Didier Rémy. Using, Understanding, and Unraveling the OCaml Language. In Gilles Barthe, editor, Applied Semantics. Advanced Lectures. LNCS 2395., pages 413–537. Springer Verlag, 2002. http://pauillac.inria.fr/~remy/cours/appsem/ocaml.pdf

[37]
M. Sipser. Introducton to the Theory of Computation. PWS Publishing, 2006.

[38]
Coq Development Team. Documentation of the coq theorem prover. http://coq.inria.fr/doc-eng.html

[39]
Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[40]
Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[41]
OCaml Development Team. The Objective Caml system:Documentation and user's manual, 2002. http://caml.inria.fr/ocaml/htmlman/index.html

[42]
Isabelle Tellier. Introduction à l'informatique. http://www.grappa.univ-lille3.fr/polys/intro-info/index.html, 2001.

[43]
D. van Dalen. Logic and Structure. Springer Verlag, Berlin, Germany, 1983.

[44]
G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge, Massachusetts, February 1993.

[45]
Bertot Y and P. Castéran. Coq'art. http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html, 2003.



Enviar comentários e dúvidas para (retire os UUU) : desousaUUU@UUUdi.ubi.pt
This document was translated from LATEX by HEVEA.