ITA | ENG
B012511 - FOUNDATIONS OF PROGRAMMING LANGUAGES
Main information
Course Content
Suggested readings
Learning Objectives
Prerequisites
Teaching Methods
Type of Assessment
Course program
Academic Year 2013-14
Coorte 2013 - Second Cycle Degree in Computer Engineering
Course year
First year - Second Semester
Belonging Department
Information Engineering (DINFO)
Course Type
Single education field course
Scientific Area
INF/01 - INFORMATICS
Credits
6
Teaching Hours
48
Teaching Term
03/03/2014 ⇒ 13/06/2014
Attendance required
No
Type of Evaluation
Final Grade
Course Content
show
Course program
show
Lectureship
Mutuality
Course teached as:
B012511 - TEORIA DEI LINGUAGGI DI PROGRAMMAZIONE
Second Cycle Degree in COMPUTER SCIENCE
B012511 - TEORIA DEI LINGUAGGI DI PROGRAMMAZIONE
Second Cycle Degree in COMPUTER SCIENCE
Course Content
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.
Suggested readings (Search our library's catalogue)
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.
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.
Prerequisites
Recommended Prerequisites: Formal Methods. Advanced programming courses. Mathematical logic.
Teaching Methods
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
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.
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.