Sistemas dedutivos lógicos e Teoria de tipos

Objectivos

Os cálculos lambda tipificados e os sistemas formais dedutivos têm um papel fundamental em várias áreas da ciência de computadores como programação funcional, semântica das linguagens de programação, demonstração automática ou processamento de linguagem natural.

Pretende-se neste módulo fazer uma introdução a estas teorias e em especial na relação existente entre elas. Considerando-se um tipo uma especificação de um programa, esta relação permite, em particular, a especificação de programas como teoremas e a obtenção de programas a partir das demonstrações desses teoremas.

Tópicos do programa

• Teoria de tipos simples para o cálculo lambda
• Lógica proposicional intuicionista
• Sistemas de dedução natural
• Isomorfismo de Curry-Howard
• Aplicações e extensões

Aulas

• Aula 1
• Aula 2
• Aula 3
• Aula 4- Sistema FTLab

Bibliografia

Gal91

Jean Gallier.
Constructive logics: Part i: A tutorial on proof systems and typed $\lambda$-calculi.
Technical report, Digital PRL, 1991.
URL:gallier91constructive.pdf.

Gen69

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

GLM97

Jean Goubault-Larrecq and Ian Mackie.
Proof Theory and Automated Deduction.
Kluwer Academic Press, 1997.

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.