| Code |
14495
|
| 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
|
|
Teaching Methodologies and Assessment Criteria |
as a course included in a PhD program, the teaching is of a theoretical nature where the research questions are introduced and contextualised, where the most relevant results are also introduced and motivated.
The students will be required to read and master the relevant literature, to be acquainted with research tools that come from the state of the art. The assessment will look for measuring these familiarity with the subject and the acquired maturity in the use of the concepts but also the research tools.--
|
|
Language |
Portuguese. Tutorial support is available in English.
|