Lógica Computacional

Licenciatura em Ciências da Computação - 2º ano

Tópicos

Avisos

Elementos Lógicos da Programação II (702752)

Licenciatura de Matemática e Ciências da Computação
2º Ano - 2º Semestre
Ano lectivo 2004/2005


Programa

Programa Resumido

  • Lambda-Calculus: teoria equacional
  • Lambda-Calculus: sistema de redução
  • Sistemas de Tipos
  • Implementação do Lambda-Calculus
  • Estudo de uma linguagem baseada no Lambda-Calculus

Programa Detalhado

Bibliografia

Bibliografia Recomendada:

  • Lambda calculi: a guide for computer scientists - Chris Hankin, Claredon Press, Oxford, 1994.
  • Theories of Programming Languages - John C. Reynolds, Cambridge University Press, 1994.
  • Introduction to combinators and lambda-calculus - J. Roger Hindley, Cambridge University Press, 1993.

Bibliografia de Referência:

  • Lambda-Calculus: Its syntax and semantics - Henk P. Barendregt, North Holland, 1985.
  • Lambda-Calculus with types - Henk P. Barendregt,in ?Handbook of Logic in Computer Science, vol.2?, Claredon Press, Oxford, 1995.
  • Proofs and Types - Jean-Yves Girard, Cambridge University Press.

Outros Elementos de Estudo

  • Módulo I: Teoria básica do lambda-calculus (pdf)
  • Módulo II: Aspectos de Implementação (pdf)
  • Módulo III: Expressividade do lambda-calculus (pdf)
  • Módulo IV: Lambda-calculus com Tipos (pdf)
  • Módulo V: Sistemas de Tipos (pdf)
  • Material aulas TP jsp: lambda.hs, SKK.pdf.

Projectos práticos

Quem desejar realizar um projecto prático no âmbito desta disciplina deve contactar um dos docentes. O objectivo desse contacto é o de obter informação/apontadores adicionais sobre os vários projectos e decidir o projecto concreto a ser realizado.

Algumas ideias para projectos práticos:

  1. Animador de uma pequena linguagem funcional com tipos.
  2. Codificação da máquina abstracta de Krivine em C .
  3. Estudo sobre o impacto da operação de substituição na avaliação de lambda-termos .
  4. Inferência/verificação de tipos numa linguagem point-free .
  5. Sobre a avaliação de lambda-termos e os monads .

Horário e Equipa docente

Horário Lectivo:

Teóricas Práticas
3ª, das 8:00 às 9:00 (sala CP3.101) TP1 , 3ª, das 14:00 às 16:00 (sala DI 0.11)
  5ª, das 15:00 às 16:00 (sala CP3.102)   TP2 , 4ª, das 10:00 às 12:00 (sala DI 0.04)  

Horário de Atendimento:

JBA
  2ª, das 14:00 às 19:00  

Critério de Avaliação

Nota final é calculada com base nas seguintes componentes:

Componente Teórica (Exame) - OBRIGATÓRIA - peso nunca inferior a 70% (nota mínima de 8 valores).
Componente Prática - FACULTATIVA - com peso máximo de 30%.

A nota para a componente prática resulta de avaliação contínua (até 2 valores) e de um trabalho prático (até 4 valores).

Notas

Notas - 1ª e 2ª Cham. (pdf)

Notas - recurso (pdf)

Época Especial:

Número Nome Exame
35846  Márcio Azevedo  5.5
43488 Paula Silva 6.5



Notas do Ano Lectivo 2005/2006 (exames)

Recurso:

Número Nome Exame FINAL
   Jácome Miguel Costa Cunha  16 16
35866  Tiago Lamas Carvalheira  1.7 REP
32738  Paulo Sérgio Azevedo Magalhães  8.7 10
38580  Jorge Filipe Morgado Marques  11.2 11

AVISO: Na pauta dos serviços académicos, não surge o nome de Jácome Miguel Costa Cunha (melhoria).

2ª Chamada:

Número Nome Exame
32738  Paulo Sérgio Azevedo Magalhães  4.5
33684  António Augusto Dias Castro Ribeiro Silva  13
35846  Márcio Azevedo  10
36867  Rui Samuel Valinho  3.5
38580  Jorge Filipe Morgado Marques  6

1ª Chamada:

Número Nome Exame
39837  Rui Miguel Pacheco Almeida  5.5
43488  Paula Cristina Gomes da Silva  12



Notas do Ano Lectivo 2006/2007 (exames)

2ª Chamada:

Número Nome Exame
39837  Rui Miguel Pacheco Almeida  10

Época Especial:

Número Nome Exame
35806 Bruno Miguel Freitas de Sousa 10

r21 - 20 Sep 2007 - 14:17:34 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM