A disciplina de Elementos Lógicos da Programação III é lecionada no 2° semestre do 3° ano da Licenciatura em Matemática e Ciências da Computação da Universidade do Minho.

Equipa Docente

José Bernado Barros (Teóricas)

Maria João Frade (Teórico-Práticas)

Horários

Aulas Teóricas
Segunda-feira 9:00-10:00
Sexta-feira 9:00-10:00

Aulas Teórico-Práticas
1° Turno --- Quinta-feira 8:00-10:00
2° Turno --- Sexta-feira 10:00-12:00

Atendimento aos Alunos
Quinta-feira, 14:00-20:00 (mjf)

Critérios de Avaliação

A avaliação da disciplina é formada por uma componente teórica concretizada através das provas finais/exames, com um peso de 65% na nota final, e de uma componente prática concretizada por respostas às questões das aula práticas laboratoriais, com um peso de 35% na nota final.

A aprovação à disciplina requer uma nota final mínima de 10 valores e uma nota mínima, em qualquer das componentes teórica ou prática, de 9 valores.

• Sebenta Teórica de Elementos Lógicos da Programação III (manuscrito), José Manuel Valença,
  Departamento de Informática, Universidade do Minho, 1996/97

 
• Introdução ao Sitema COQ de Assisteência à Prova, (Elementos Lógicos da Programação III)
  Jorge Sousa Pinto e Maria João Frade
  Departamento de Informática, Universidade do Minho, 1997/98

 
• Guiões das Aulas Laboratoriais + Ficheiros Coq



• Guião 1 - Declarações, Definições, Inferencia de Tipos Simples e Redução de Termos.
  a1elp3.v
• Guião 2 - O Cálculo da Construções.
  a2elp3.v
• Guião 3 - O Mecamismo de Prova - Lógicas Mínimas.
  a3elp3.v
• Guião 4 - O Mecamismo de Prova - outros tópicos.
  a4elp3.v
• Guião 5 - Introdução aos Tipos Indutivos - os números naturais.
  a5elp3.v
• Guião 6 - Tipos Indutivos - exemplos.
  a6elp3.v
• Guião 7 - Introdução á Verificação e Síntese de Programas em Coq
  a7elp3.v

 
• Folhas de Exercícios
  
  
  • Ficha 1 - Lambda-Calculus com Tipos
  • Ficha 2 - Formação de Contextos, Termos e Tipos.
 
 
• Documentação sobre o sistema COQ versão 6.1 - all-docs.tar.gz
  
  
  • The Coq Proof Assistant - A Tutorial, version 6.1, Project Coq
    INRIA-Rocquencourt - CNRS - ENS Lyon, 1996
     
  • The Coq Proof Assistant - Reference Manual, version 6.1, Project Coq
    INRIA-Rocquencourt - CNRS - ENS Lyon, 1996
     
  • The Coq Proof Assistant - The Standard Library, version 6.1, Project Coq
    INRIA-Rocquencourt - CNRS - ENS Lyon, 1996

• Visite o nosso ftp site
• The COQ Proof Assistant
• Logical Frameworks

Disciplinas leccionadas pelo Departamento de Informática

Qualquer sugestão, correcção ou comentário poderá ser enviada para Maria João Frade.