Home
Courses
Computer Science and Engineering
Proof and Programming Language Theory

Proof and Programming Language Theory

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
Language	Portuguese. Tutorial support is available in English.