Academics
Computational Logic 1
(Lógica Computacional 1)
this
is a semester course for computer science undergraduate
students on predicate and propositional and predicate logic and their applications in computer science mainly for verification. Although concepts such as correctness and completeness and incompleteness are reviewed the emphasis is on deductions methods and their applications in specification, formalization and verification.
Didactic material of the course, semester 2012/I
Foundations of logic and functional programming
((Introdução à) Teoria da Computação)
this is a semester course for mathematic and computer science engineering graduate students on mathematical foundations of computation, specifically, from the point of view of the logic and functional programming paradigms. Logic resolution principle, unification, SLD-resolution, its completeness and its soundness are formally studied. Rewriting theory is examined as the more appropriate formalism for reasoning about the functional programming paradigm. Both paradigm are checked showing that their expressiveness is enough to allow the specification and computation of the computable functions.
Didactic material of the course, semester 2011/II
Topics in Computation: Type Theory
(Tópicos em Computação: Teoria dos Tipos)
this is a semester course
for mathematics and computer science graduate students on foundations of type theory and its applications to semantics and logic of computation.
Untyped lambda calculus and its typed versions making emphasis on the simple typed case à la Church and à la Curry are covered. Type checking, type inference and the problem of inhabitation are considered.
Bibliography:
- H.P. Barendregt,
Lambda Calculus with Types. Chapter in Handbook of Logic in Computer Science, Vol. 2, pages 117-309, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, eds., Clarendon Press | Oxford, 1992.
1974.
- J.R. Hindley, Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, n. 42, Cambridge University Press, 1997.
- H. Simmons, Derivation and Computation: Taking the Curry-Howard Correspondence Seriously. Cambridge Tracts in Theoretical Computer Science, n. 51, Cambridge University Press, 2000.
- A. Church,
A Formulation of the Simple Theory of Types Journal of Symbolic Logic, 5:56-68, 1940.
- Kamareddine, F. D. and T. Laan and R. Nederpelt,
A Modern Perspective on Type Theory Applied Logic Series 29, Kluewer, 2004.
- F. Kamareddine, T. Laan and R. Nederpelt, Types in logic and mathematics before 1940, in Bull. Symbolic Logic, 8(2):185-245, 2002.
- Online Resources from Peter Aczel URL: http://www.cs.man.ac.uk/~petera/Types_course/types_resources.html
-
Lecture notes
- by Ralph Loader (39 pages)
-
The impact of the lambda calculus in logic and computer science -
by Henk Barendregt
-
Foundations of Functional Programming Lecture Notes, by Larry Paulson (54 pages)
-
Lambda Calculi with Types,
by Henk Barendregt, Handbook of Logic in Computer Science, Volume II (193 pages)
-
Proof Assistants using Dependent Type Systems
, by Henk Barendregt and Herman Geuvers, Handbook of Automated Reasoning,
edited by Alan Robinson and Andrei Voronkov, 2001, (89 pages)
- Lecture notes, by Luke Ong (89 pages)
-
Lectures on the Curry-Howard Isomorphism
by Morten Heine B. Sorensen (University of Copenhagen),
Pawel Urzyczyn (University of Warsaw)
(275 pages)
-
Type Systems, By Luca Cardelli (42 pages)
An introductory overview
-
Lecture Notes by
H. Schwichtenberg
-
Introduction to the Literature on Semantics,
by Gary T. Leavens
- Ementa primeiro semestre de 2011 ( PDF) In Portuguese.
Research Topics in Computation: Formal Methods
Summer course offered by the Graduate Program in Informatics, Summer Semester 2010 (Prof. Mauricio Ayala Rincón and Cesar Muñoz, NASA Langley Research Center)
A short course also offered at ITIV, Karlsruher Institute für Technologie
(Prof. Mauricio Ayala Rincón)
this
is a summer course on fundamentals of formal methods and proof technologies in the proof assistant PVS.
foils and
exercises for the short course at ITIV.
Computational
Complexity and Computability (Complexidade Computacional e Computabilidade):
Offered by the Graduate Program of the Departamento de Matemática, First Semester 2010
(Prof. Mauricio Ayala Rincón)
this is a semester course
for mathematics and computer science graduate students on foundations of theory of complexity: the study of why some problems are so hard to solve by computers and, in general, the classification of problems with respect to the necessary computational resources of its solutions. Turing Machines are reviewed introducing the classic computational complexity
classes according to the use of computational (time/space) resources. Relations
between computational complexity classes are studied from the structural
point of view. NP-complete and PSPACE-complete problems are
examined. Also, probabilistic algorithms, that result from approximate solution for intratable problems, as well as the corresponding probabilistic classes are considered.
Bibliography:
- S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009.
- S. Homer and A. L. Selman, Computability and Complexity Theory, Texts in Computer Science, Springer, 2001.
- D.P. Bovet and P. Crescenzi, Introduction
to the Theory of Complexity, C.A.R. Hoare Series Editor. Prentice-Hall,
1994.
- J.L. Balcázar and J. Díaz and J. Gabarró,
Structural Complexity I, EATCS monographs on Theoretical Computer
Science. Springer, econd edition, 1995.
- C.H. Papadimitriou, Computational Complexity,
Addison-Wesley Publishing Company, 1994.
Details
of the last program of the course, second semester 2005 (in Portuguese) (postscript) (PDF)
Topics in computation: proof theory (Tópicos em Computação: teoria de prova)
this is a semester graduate course
for computer science and mathematics students on proof theory.
The course brings a solid background for students who pretend to do research in automated deduction and formal methods.
Bibliography:
- A. S. Troelstra and H. Schwitchtenberg, Basic Proof Theory Cambridge Tracts in Theoretical Computer Science, CUP 2000.
- S. R. Buss (Ed), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, Vol. 137, North Holland, Elsevier, 1998.
- S. Negri and J. von Plato, Structural Proof Theory CUP 2001.
- P. Aczel, H. Simmons and S. Wainer (Eds), Proof Theory CUP 1994.
Analysis of Algorithms
(Análise de Algoritmos)
Offered by the Undergraduate Program of the Departamento de Matemática, First Semester 2009
(Prof. Mauricio Ayala Rincón)
this
is a semester course for mathematic and computer science undergraduate
students on design and analysis of computer algorithms. Regularly, simple
computer data structures and a collection of efficient algorithms for classical
computer science problems, such as sorting, searching, string pattern matching,
graph theory problems, mathematical problems, etc. are studied. Also, basic
computer programming techniques are presented: divide and conquer, dynamic
programming, etc. The course includes a brief introduction on algorithmic
complexity classes and parallel models of computation.
Didactic material of the course, semester 2009/I
Introduction to Formal Logic (313998 Introdução à Lógica Formal)
Offered by the Graduate Program of the Departamento de Matemática, First Semester 2009
(Prof. Mauricio Ayala Rincón)
this is a semester course for mathematics and computer science graduate students on formal logic. The focus is on the expressiveness and limitations of first-order logic. Gödel completeness and incompleteness theorems are carefully studied and Lindström theorems on the maximality of first-order logic as a language to formalize mathematics which satisfies the compactness property and the Löwehneim-Skolem property. The course brings a solid background for mathematics and computer science students who want research in formal methods, proof and type theory.
Bibliography:
- H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic. Springer, 1984.
- W. Rautenberg, Einfürung in die Mathematische Logik. Vieweg, 2002.
- H. B. Enderton, A Mathematical Introduction to Logic. Academic Press Inc., 1972.
- A. Yasuhara, Recursive Function Theory and Logic. Computer Science and Applied Mathematics. Academic Press, 1971.
Topics in Computation: advanced rewriting theory (Tópicos em Computação: teoria de reescrita avançada)
Offered by the Graduate Program of the Departamento de Matemática, Second Semester 2007
(Prof. Mauricio Ayala Rincón)
this is a semester course for mathematics and computer science graduate students on advanced topics on rewriting theory.
Bibliography:
- F. Baader and T. Nipkow, Term Rewriting and All That
Cambridge University Press, 1998.
- TERESE Term Rewriting Systems by Terese, Cambridge Tracts in Theoretical Computer Science. CUP 2003.
Advanced Automata Theory and Formal Languages (Linguagens Formais e Autômatos II):
this is a semester graduate course
for mathematics students on algebraic foundations of formal language and computational model theory.
The goal of the course is the presentation of the regular and context free languages and their associated models in an algebraic setting.
Bibliography:
- D. Kozen, Automata and Computability Springer-Verlag, 1997.
- C.C. Sims, Computation with Finitely Presented Groups (Chapter 3), CUP 1994.
Numerical Calculus (Cálculo Numérico)
this is a undergraduate course on foundations of numerical calculus for mathematics, physics and engineering students.
Didactic material of the course, semester 2005/I
Topics in Computation: Formal Logic and Computability (Tópicos em Computação: Lógica formal e computabilidade)
this is a semester course for mathematics and computer science graduate students on formal logic and computability.
Bibliography:
- G. S. Boolos, J. P. Burgess, and R. C. Jeffrey, Computability and Logic. Cambridge University Press, fourth edition, 2002.
- H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic. Springer, 1984.
- H. B. Enderton, A Mathematical Introduction to Logic. Academic Press Inc., 1972.
- A. Yasuhara, Recursive Function Theory and Logic. Computer Science and Applied Mathematics. Academic Press, 1971.
Topics in Foundations and Methods of Computation: Algorithms for Computational Biology (Tópicos em Fundamentos e Métodos da Computação: Algoritmos para biologia computacional)
this is a semester course for mathematics and computer science graduate students on formal logic and computability.
Bibliography:
- D. Gusfield, Algorithms on Strings, Trees and Sequences: Computer Science and Computational Biology. Cambridge University Press, 1997.
- J. C. Setubal and J. Meidanis, Introduction to Computational Molecular Biology . PWS Publushing Company, 1997.
- D. Voet and J. G. Voet, Biochemistry. John Wiley and Sons, 1990.
- Michael S. Waterman, Introduction to Computational Biology: Maps, Sequences and Genomes. CRC Press, 1995.
- P. A. Pevzner, Computational Molecular Biology: An Algorithmic Approach. MIT Press, 2000.
- R. Durbin, S. R. Eddy, A. Krogh and G. Mitchison, Biological Sequence Analysis : Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, 1999.
- Bryan Bergeron, Bioinformatics Computing. Prentice Hall PTR, 2002.
Analysis and Complexity of Algorithms
(Projeto e Complexidade de Algoritmos):
this
is a semester course for computer science graduate
students on advanced design and analysis of computer algorithms.
The course includes a very brief introduction on
complexity theory.
Bibliography:
- S. Baase and A. van Gelder Computer Algorithms, Introduction
to Design and Analysis, Third Edition. Addison-Wesley, 1998.
- A. H. Aho, J. E. Hopcroft and J. D. Ullman,
The Design and Analysis of Computer Algorithms. Addisson-Wesley,
1974.
- T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein,
Introduction to Algorithms - Second Edition -. MIT press, 2001.
- D. Gusfield,
Algorithms on Strings, Trees and Sequences. Cambridge University Press, 1997.
- J. von sur Gathen and J. Gerhard,
Modern Computer Algebra. Cambridge University Press, 1999.
Grades (Menções) 2003 I
Automata Theory and Formal Languages (Linguagens Formais e Autômatos):
this is a semester undergraduate course
for computer science students on foundations of formal language and models of computation.
Goals of the course are presentation of the Chomsky Hierarchy and computability notions from a formal point of view. Regular, context free, context sensitive and recursive enumerable languages are studied presenting their corresponding grammars and model
s of computation: finite automata, pushdown automata, linear bounded automata and Turing Machines, respectively. Turing machines are reviewed presenting the Church-Turing Thesis and undecidability examples.
Didactic material of the course, semester 2003/I
Topics in Computation: Category Theory and Computation (Tópicos em Computação: Teoria de Categorias e Computação):
this is a semester course for mathematics and computer science graduate students on category theory and its applications in computer science.
Bibliography:
- P. Blauth Menezes , E. H. Haeusler, Teoria das Categorias para Ciência da Computação. Sagra Luzzatto, 2001,
- R. F. C. Walters, Categories and Computer Science. Cambridge Computer Science Texts,
1991.
- R. Bird and O. de Moor, Algebra of Programming. C.A.R. Hoare Series Editor, 100th Title, Prentice Hall International Series in Computer Science,
1997.
Topics in Computation: Advanced Type Theory (Tópicos em Computação: Teoria dos Tipos Avançada)
this is a semester course
for mathematics and computer science graduate students on advanced topics of type theory and its applications to semantics and logic of computation.
The problem of inhabitation, dependant and intersection types, typed explicit substitutions calculi and the Barendregt cube are studied.
Bibliography:
- H.P. Barendregt,
Lambda Calculus with Types. Chapter in Handbook of Logic in Computer Science, Vol. 2, pages 117-309, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, eds., Clarendon Press | Oxford, 1992.
1974.
- J.R. Hindley, Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, n. 42, Cambridge University Press, 1997.
- J.C. Mitchell, Foundations for Programming Languages. MIT Press, 1996.
Seminar on Categories and Computer Science (Seminário de Computação):
this is a semester seminar course
for mathematic and computer science graduate students on foundations of theory of categories and its applications to computer science.
In particular, we are interested in the study of applications of categorical methods to rewriting theory.
Bibliography:
- R. F. C. Walters, Categories and Computer Science. Cambridge Computer Science Texts,
1991.
- R. Bird and O. de Moor, Algebra of Programming. C.A.R. Hoare Series Editor, 100th Title, Prentice Hall International Series in Computer Science,
1997.
- E. Moggi and G. Rosolini (Eds),
Category Theory and Computer Science, Seventh Int. Conference, CTCS'97, Santa Margherita Ligure, Italy, September 1997. Lecture Notes in Computer Science 1290. Springer, 1997.
- F. Baader and T. Nipkow, Term Rewriting and All That
Cambridge University Press, 1998.
Seminar on Computational
Complexity (Seminário de Computação):
this is a semester seminar
for mathematic graduate students on foundations of theory of complexity.
Turing Machines are reviewed introducing classic computational complexity
classes according to the use of computational resources time/space. Relations
between computational complexity classes are studied from the structural
point of view. NP-complete and PSPACE-complete problems are
examined. Probabilistic algorithms and classes as well as the polynomial
time hierarchy are studied too.
Bibliography:
- D.P. Bovet and P. Crescenzi, Introduction
to the Theory of Complexity, C.A.R. Hoare Series Editor. Prentice-Hall,
1994.
- J.L. Balcázar and J. Díaz and J. Gabarró,
Structural Complexity I, EATCS monographs on Theoretical Computer
Science. Springer, econd edition, 1995.
- C.H. Papadimitriou, Computational Complexity,
Addison-Wesley Publishing Company, 1994.
Details
of the last program of the course, first semester 1997 (in Portuguese)
Calculus I (Cálculo Diferencial e Integral):
Introduction to the Theory of Graphs (Introdução à Teoria dos Grafos):
this is a semester course
for mathematics and computer science undergraduate students on foundations of theory of graphs, that is given from the algorithmic point of view: diverse applications of this formalism for modeling very simple real problems are given and, subsequently, efficient computational solutions are discused. Topics covered range from the very simple algorithms for searching paths in graphs to the graph coloring problem.
Bibliography:
- A. H. Aho, J. E. Hopcroft and J. D. Ullman,
The Design and Analysis of Computer Algorithms. Addisson-Wesley,
1974.
- R. Sedgewick, Algorithms in C++. Addison-Wesley,
1992.
- T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein,
Introduction to Algorithms - Second Edition -. MIT press, 2001.
- N. Christofides,
Graph Theory An Algorithmic Approach Academic Press, 1975.
- S. Even,
Graph Algorithms Computer Science Press, 1979.
Other courses I
like:
- Undergraduate courses:
- Graduate courses:
- Foundations of Mathematical Logic Usually offered by Prof. Haydeé Werneck Poubel first semester every year
- Analysis of Algorithms and Computer Structures
- Formal Languages II
--> Could be offered second semester 2000 according to alumni interest!
- Seminar on Mathematical Logic
- Computational Complexity