Introdução aos assistentes de demonstração usando o COQ

Objectivos

Introdução aos assistentes de demonstração automática usando o COQ.

Tópicos do programa

1. Teoria de tipos simples para o lambda-calculus, dedução natural e isomorphismo de Curry-Howard
2. Sistemas de Tipos dependentes e introdução ao cálculo de construções indutivas
3. Uso do sistema Coq para teoremas da lógica de predicados e sistemas de tipos indutivos
4. Exemplos de desenvolvimento de especificações de programas simples.

Aulas 06/07

13/11/06,18h

Aula 1

• Introdução ao COQ
• Tutorial do COQ
• Exemplos (init, minimal)

15/11/06,18h

Aula 2

• Exemplos (logic, nats, lists, bin,indpred, insertion, RecTutorial)
• Tutorial sobre tipos inductivos

Aulas 05/06

7/12/05,18h

Aula 1

13/12/05,18h30m

Aula 2

• Introdução ao Sistema COQ: Expressoes e tipos; hiearquia de tipos; Espécies Set e Prop; Proposicoes e demonstracoes; Tácticas: intro, apply, assumption.
• Exemplos (init, minimal)

14/12/05,18h

• Tipos dependentes. Regras de Tipificação. Lógica de primeira ordem e Tipos dependentes. Tipos indutivos. Regras de introdução e eliminição.
• Resumo de tácticas
• Exemplos (pred, induc,plane,vec)

15/12/05,18h

• Tipos indutivos recursivos, polimorficos e dependentes.Predicados indutivos. A biblioteca do COQ.
• Exemplos (nats, lists, bin,indpred, insertion, RecTutorial)

Avaliação 05/06

20-21/12/05 das 18h às 18h30m no Lab. 01.

Exemplo de perguntas de teste:

• Mostrar que

  forall A B C: Prop, A /\ (B /\ C) -> (A /\ B) /\ C

  Sem usar a táctica auto (ou equivalente)

• Usando a definição de tipo indutivo even e o tipo nat dados no curso, mostrar que

  forall n m:nat, even n -> even m ->even (n+m).

Material

• Lectures on Curry-Howard Isomorphism

• Tutorial do COQ
• Tutorial sobre tipos inductivos

• Manual de Referência do COQ

• COQ na Types Summer school 2005

• Proof assistants using dependent type system, H. Barendregt and H. Geuvers

• Constructive logics: Part i: A tutorial on proof systems and typed $\lambda$ mathend000#-calculi. J. Gallier Technical report, Digital PRL, 1991.

O livro Coq'Art existe na biblioteca do DCC e tem uma versão online em francês...

Ligações

COQ Homepage

Temas de Tese

Possíveis temas para teses de mestrado (em co-orientação com Rogério Reis):

• Desenvolvimento de um módulo COQ sobre autómatos finitos e linguagens regulares.
• Desenvolvimento de um módulo COQ sobre Algebras de Kleene e algebras de Kleene com testes. Estas últmas são equivalentes a lógicas de Hoare e permitem a especificação de propriedades de programas.
• Interface da ferramenta de verificação de especificações de programas Why para o Python.

Bibliografia

BC04

Yves Bertot and Pierre Castéran.
Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS Series. SV, 2004.

Gen69

Gerhard Gentzen.
Investigations into logical deduction.
In The Collected Papers of Gerhard Gentzen, chapter 3. North-Holland, 1969.

Hin97

J. Roger Hindley.
Basic simple type theory.
Number 42 in Cambridge Tracts in Theoretical Computer Science. CUP, 1997.

PU96

Morten B. Sorensen Pawel Urzyczyn.
Lecture on the curry-howard isomorphism.
Technical report, University of Copenhagen, 1996.
http://zls.mimuw.edu.pl/ urzy/ftp.html.