Overall objectives:

1 - Study of the limits of computing.
2 - Practice of programming with "go to's" and of definition of functions.
3 - To acquire knowledge of the algebraic and logical foundations of some of the programming paradigms already studied by the students (imperative; recursive; and rewrite and use of abstract types).

Syllabus:

1 - Computability Theory.
1.1 - Unlimited Register Machine (URM) and URM-computable functions.
1.2 - Generation of the URM-computable functions; primitive recursive functions and partial recursive functions.
1.3 - Turing machine and Turing-computable functions, and reference to other approaches to computability. Church's thesis.
1.4 - Coding URM-programs. The diagonal method. Proof of the existence of non-computable functions. The s-m-n Theorem.
1.5 - Universal programs. Decidability, undecidability and partial decidability.
2 - Algebraic and Logical Foundations of Computation.
2.1 - Hoare calculus and proof of the correcteness of imperative programs (with respect to its specification).
2.2 - Definition of functions using recursion. Proof of the correctness of recursive programs using transfinite induction (on well-ordered sets).
2.3 - Equational specifications of abstract data types. Language. Equational calculus. Rewriting.

Literature/Sources:

A.G. Hamilton , 1988 , Logic for Mathematicians , Cambridge University Press
Carmo, J., Gouveia, P e Dionísio, F. , 2013 , Elementos de Matemática Discreta , College Publications
N.J. Cutland , 1980 , Computability - An Introduction to Recursive Function Theory , Cambridge Press
A. Sernadas & C. Sernadas , 1999 , Fundamentos Algébricos da Engenharia da Programação , Instituto Superior Técnico
G. Boolos e R. Jeffrey , 1990 , Computability and Logic , Cambridge University Press
D. Bridges , 1994 , Computability: A Mathematical Sketchbook , Springer-Verlag
B.F. Chellas , 1980 , Modal Logic: An Introduction , Cambridge University Press
F. Coelho e J.P. Neto , 2010 , Teoria da Computação - Computabilidade e Complexidade , Escolar Editora
M. Davis , 1983 , Computability and Unsolvability , Dover
M. Davis e E. Weyuker , 1983 , Computability, Complexity and Languages , Academic Press
P. Dume , 1991 , Computability Theory: Concepts and Applications , Ellis Horwood
H. Ehrig e B. Mahr , 1985 , Fundamentals of Algebraic Specification I , Springer Verlag
R.L. Epstein e W.A. Carnielli , 1999 , Computability: computable functions, logic and the foundations of mathematics , Wadsworth
R. Goldblat , 1982 , Axiomatising the Logic of Computer Programming , Springer
R. Goldblat , 1992 , Logics of Time and Computation , CSLI
V.J. Rayward-Smith , 1995 , A First Course in Computability , McGraw-Hill (computer Science Texts)
C. Sernadas , 1993 , Introdução à Teoria da Computação , Editorial Presença
A. Sernadas e C. Sernadas , 2012 , Fundamentos de Lógica e Teoria da Computação , College Publications

Assesssment methods and criteria:

Classification Type: Quantitativa (0-20)

Evaluation Methodology:
Theoretical expository lectures, illustrating the concepts through various examples. Practical problem solving classes. The evaluation is made by means of two written tests, each of them weighted 50% in the final classification.