The course presents the fundamental concepts and techniques in a foundational approach to programming languages. The central thread is to see is a single program that a complete language as a mathematical object, on which you can assert and prove certain properties. Central topics are: techniques of operational semantics for the formal definition of languages and systems of its type and properties of correctness, and subtype polymorphism, fundamentals of object-oriented languages.
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Learning Objectives
At the end of the course, students should have acquired the following competences:
1) A rigorous approach, based on type theory, the study of problems related to the design of languages, their extensions and implementations.
2) Ability to use formal techniques to try to study the properties of the programs.
3) A preparation sufficiently deep (on semantics and types) to allow the deepening of research publications on the topics discussed.
Number of hours for personal study and other individual learning: 90
Number of hours for classroom activities: 48
Number of hours for seminars to: 12
Type of Assessment
Activities of seminars by students. Final oral examination.
Course program
The course presents the concepts and techniques central to a foundational study of programming languages, together with their bases logichee formal. The central thread is to see is a single program that a complete language as a mathematical object, on which you can assert and prove certain properties with rigorous techniques.
The course is as follows:
1) Programming Fundamentals-functional, inductive definitions and formal methods of proof. Operational semantics.
2) Systems of the type-typed lambda-calculus simple, mandatory references and type-safety. Metatheory of the definition disottotipo.Algoritmidi type-checking. Polymorphism and type inference.
3) Case study: Featherweight Java (a model of the heart of java). Generic types. Proof of Safety. Intersection types and wildcards.
4) Advanced Topics, as the existential types and / or polymorphism of a higher order.