SISTEMAS DE TIPOS

Curso de Pós-Graduação no ICEX-UFMG

Prof: Carlos Camarão de Figueiredo
Click here for an English version of this page

Programa do Curso:

• Introdução à Lógica de primeira ordem
• Introdução ao Lambda-calculus : sintaxe, convenções de notação, variáveis livres e ligadas, regras de conversão, igualdade, extensionalidade, substitutição. Representando coisas no lambda-calculus: valores-verdade, pares e tuplas, recursão, funções recursivas.
• Sistemas de Tipos : Introdução (propósitos de tipagem), lambda-calculus tipado, regras de tipo, lambda-calculus tipado de segunda ordem, lambda-calculus tipado polimórfico

Quem deve assistir:

• estudo de questões fundamentais da computação
• projeto de linguagens de programação
• sintaxe e semântica de linguagens
• programação funcional

Porque você gostará desse curso:

• O curso é fácil; o material do curso procura fazer com que os assuntos fiquem agradáveis e divertidos
• Os tópicos são da maior importância, se você é um estudante bom e interesado em ciência da computação
• O curso lhe dará informações valiosas e colocará você muito perto de uma tese, se estiver interessado em fazer uma tese envolvendo alguns tópicos em alguma das áreas relacionadas acima
• A avaliação não dará peso grande a provas, mas aos seminários e exercícios
• Os estudantes terão tempo de aula disponível para ler, pensar, discutir e preparar seminários e fazer exercícios

Bibliografia:

• Para a primeira parte do curso: disponível daqui a pouco...
• As aulas na segunda parte do curso (sobre introdução ao lambda-calculus) serão baseadas em:
  

  Introduction to Functional Programming
  Mike Gordon
  Notas de aula e conjunto de transparências, Cambridge, UK, 1996.

  O conjunto de transparências está então disponível nesse nó!
  
  Outros materiais a serem usados nesta parte do curso são:
  • Capítulo 2 de:

    Type Theory and Functional Programming
    Simon Thompson (University of Kent at Canterbury)
    Addison-Wesley, 1991.

  • Capítulo 1 de:

    The Implementation of Functional Programming Languages
    Simon Peyton Jones (University of Glasgow, Scotland)
    Prentice Hall, 1987.

    Estes livros estão disponíveis na biblioteca do departamento.
• A terceira parte do curso será baseada em:

  An Introduction to Polymorphic Lambda Calculus with Subtyping
  Kim Mens, Relatório técnico, Vrije Universiteit Brussel, 1994.

  Disponível via WWW.
  
  Outros materiais a serem usados nesta parte do curso são:
  • O artigo:

    Type Systems
    Luca Cardelli (DEC/SRC), 1996.

    Disponível via WWW.
  • O artigo:

    Type Systems for Programming Languages
    John Mitchell (Stanford University)
    in Handbook of Theoretical Computer Science, The MIT Press/Elsevier, 1990.

    Disponível na biblioteca do departamento.

Avaliação:

• Cada estudante deverá participar da apresentação de dois seminários, de 20 pontos cada. Cada seminário será dado por um grupo de estudantes. O assunto do primeiro seminário é lambda-calculus: um grupo baseará seu seminário no livro de Simon Thompson e o outro grupo no livro de Peyton Jones.
• Cada estudante fará algumas listas de exercícios, que totalizarão 30 pontos.
• Cada estudante deverá fazer dois exames, de 15 pontos cada.