You need to activate javascript for this site.
Menu Conteúdo Rodapé
  1. Home
  2. Courses
  3. Computer Science and Engineering
  4. Proof and Programming Language Theory

Proof and Programming Language Theory

Code 11508
Year 1
Semester S1
ECTS Credits 6
Workload OT(15H)
Scientific area Informatics
Entry requirements --
Mode of delivery face-to-face
Learning outcomes This course aims to address the fundamental topics of proof and programming as a uniform discipline.
Upon completion of the course, the students should be able to:
- Model, formalize and develop proof using a computer
- Mathematically model programs
- Understand, define and extend the semantics of programming languages
- Understand, define and use mathematical programming models and formal proofs
Syllabus
This course aims to address the fundamental topics of mechanized proof and programming. In particular this courses covers in a uniform and unifying way the proof theory and the theory of programming, that is the definition and the implication of the Curry-Howard isomorphism.
The course therefore exposes the conceptual foundations, techniques and tools that explain, justify and design the reasoning as well as computer programs based for this purpose on the comprehensive and uniform theoretical framework of the type theory, logic and formal semantics.
Main Bibliography José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development An Introduction to Program Verification. Springer Verlag, 2010.

Morten Heine B. Sørensen , Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism (1998)


John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.

B. A. Davey and H. A. Priestley. Introduction to Lattices and Order: 2nd Ed.. Cambridge University Press, 2002.

Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 2, pages 117?309. Oxford University Press, 1992.

A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory
Cambridge Tracts in Theoretical Computer Science(No. 43)
2nd Edition, 2000.


H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons, Chichester, 1993
Planned learning activities and teaching methods In order to evaluate the acquired skills, the teaching-learning activities will evaluate both the understanding of theoretical concepts as well as the ability to put them in practice.

Theoretical assessment: A critical analysis of two scientific papers of the area proposed by the teaching staff.

Practical assessment: practical exercises delivered to the teaching staff (study, modeling, design, implementation and talk).
Metodologias de Ensino e Critérios de Avaliação Avaliação teórica : 50% da avaliação global (avaliação de trabalhos de natureza teórica) Avaliação prática: 50% da avaliação global (avaliação de trabalhos de natureza prática)
Language Portuguese. Tutorial support is available in English.
Last updated on: 2014-08-07

The cookies used in this website do not collect personal information that helps to identify you. By continuing you agree to the cookie policy.