MAP/i - Programming Paradigms

Program Semantics, Verification, and Construction

Overview.

The reliability of computing systems plays an essential role in modern society, where so many areas of human activity depend on technology. The deliverables of software projects may no longer be limited to code; the ability to produce certified code is now crucial. Code may be certified as being functionally correct, or as possessing certain execution properties (for instance, a program may be certified as not trying to access unauthorised resources).

The ability to certify software in this way requires a sound knowledge of the theory of programming languages and mathematical reasoning tools, as well as acquaintance with tool-assisted techniques. This course gives an overview of the theory of programming languages at an advanced level and then goes on to apply the theory to methods for obtaining correct, certified software.

Aims.

• to present in a systematic way a vast set of results in fundamental areas of Theoretical Computer Science, in particular Logic, Lambda-calculus, Type Theory and Programming Language Semantics, as well as the relationships between them;
• to introduce several rigorous approaches to the production of correct software, namely in:
  • Program Verification , the activity that aims to establish that a program effectively behaves according to its specification, or that its behaviour is characterised by a set of given properties;
  • in Mathematical Program Construction , a method for obtaining correct programs from specifications, strongly based on program calculation.

Lecturing Team.

The team consists of members of the Department of Informatics of the University of Minho and the Department of Computer Science of the University of Porto (Faculty of Science). All team members are working, and have worked actively in the past few years, on topics that are directly related to the subjects covered by this course, as detailed below.

• José Bacelar Almeida (DI-UM) has worked on the verification of security protocols, and has experience in using proof-assistants for program development.
• Sabine Broda (DCC-FCUP) has worked on Mathematical Logic, lambda-calculus, and Type Theory.
• Luís Damas (DCC-FCUP) has worked extensively on lambda-calculus and Type Theory; he is in fact responsible for the introduction of many of these subjects in Portugal.
• Mário Florido (DCC-FCUP) has worked on lambda-calculus, type systems, and program transformation.
• Maria J. Frade (DI-UM) has worked on lambda-calculus, type systems, and Proof Theory.
• Nelma Moreira (DCC-FCUP) has worked on Automata Theory, Proof Theory, and proof assistants.
• José N. Oliveira (DI-UM) has worked extensively on Formal Methods in Software Engineering and is in fact a pioneer of this area in Portugal. Recently he has become interested in the calculation-based approach to program construction.
• Jorge Sousa Pinto (DI-UM) has worked on Linear Logic, lambda-calculus, and functional program transformation.