Teoria da Computação
(cod.2813)

Departamento de Informática
Universidade da Beira Interior

Ano lectivo 2005/2006

Esta página no formato pdf, no formato ps

1  Novidades


Conteúdo

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

Encontrará aqui o escalonamento previsto das aulas.

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

8  Trabalho Prático

9  Horário

Tipo de aula Horário Sala
Teórica Terça-Feira das 9h00 às 11h00 6.02
Teórica-Prática 1 Quarta-Feira das 8h00 às 9h00 6.18
Prática 1 Quarta-Feira das 10h00 às 12h00 6.14
Teórica-Prática 2 Quarta-Feira das 12h00 às 13h00 6.19
Prática 2 Quinta-Feira das 9h00 às 11h00 6.14
Teórica-Prática 3 Quarta-Feira das 9h00 às 10h00 6.16
Prática 3 Quinta-Feira das 11h00 às 13h00 6.14

10  Atendimento

Horário
Quarta-Feira das 14h00 às 17h00

11  Alunos de Engenharia Informática inscritos

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]
H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons, Chichester, 1993. http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
[31]
L. Pequet. Programmation fonctionelle - introduction illustrée en objective caml. http://www-rocq.inria.fr/~pecquet/pro/teach/teach.html, 2002.
[32]
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
[33]
A. Pitts. Lecture notes on computation theory. University of Cambridge Computer Laboratory, 2002. http://www.cl.cam.ac.uk/Teaching/2002/CompTheory
[34]
F. Prost and G. Kahn. Checking mathematical facts with coq: Various examples of Coq proofs. http://coq.inria.fr/contribs-eng.html
[35]
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
[36]
Coq Development Team. Documentation of the coq theorem prover. http://coq.inria.fr/doc-eng.html
[37]
Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html
[38]
Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html
[39]
OCaml Development Team. The Objective Caml system:Documentation and user's manual, 2002. http://caml.inria.fr/ocaml/htmlman/index.html
[40]
Isabelle Tellier. Introduction à l'informatique. http://www.grappa.univ-lille3.fr/polys/intro-info/index.html, 2001.
[41]
D. van Dalen. Logic and Structure. Springer Verlag, Berlin, Germany, 1983.
[42]
G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge, Massachusetts, February 1993.
[43]
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.