Babes-Bolyai University of Cluj-Napoca
Faculty of Mathematics and Computer Science
Study Cycle: Master

SUBJECT

Code
Subject
MID1004 Formal Models in Programming Languages
Section
Semester
Hours: C+S+L
Category
Type
Component-Based Programming - in English
2
2+1+1
speciality
compulsory
Formals Methods in Programming - in English
2
2+1+1
speciality
compulsory
Modeling and Simulation - in English
2
2+1+1
speciality
compulsory
Teaching Staff in Charge
Assoc.Prof. MOTOGNA Simona Claudia, Ph.D.,  motognacs.ubbcluj.ro
Aims
The goal of this course is to introduce students to fundamental ideas behind the design and analysis of modern programming languages. In the first part, we focus on the study of different approaches for specifying models for programming languages. We will study semantic analysis inside a compiler as a first formal model of the meaning associated with syntactical constructions, operational semantics for specifying how programs compute, and denotational semantics for specifying what programs compute.
In the end, the students should be able to:
• Explain the differences between informal and formal semantics of programming languages, and between the operational and denotational and axiomatic approaches to formal semantics.
• Read a formal model for a small programming language, interpret it in informal terms, and predict how a given program will behave according to the semantic definition.
• Carry out mathematical proofs of very simple properties of a language and particular programs, given a formal model of the language.
Content
The course will be structured in three big chapters, starting with an introduction to formal methods in programming language specification. It will consist of: formal specification of syntactical constructions inside a compiler, and then operational and denotational models for programming languages. The course will propose models for language constructions, such as: types, expressions, statements, functions, subtyping, and for different types of languages: imperative, functional, logical, object-oriented. For different models the problrm of semantic equivalence will be discussed.
References
1. BAUER, F.L. - WOSSNER, H.: Algorithmic language and program development, Springer-Verlag, Berlin,1982.
2. GRUNE, DICK - BAL, H. - JACOBS, C. - LANGENDOEN, K.: Modern Compiler Design, John Wiley, 2000
3. GUNTER, C. – Semantics of programming languages, MIT Press, 1992
4. Hennessy, M. - The Semantics of Programming Languages. Wiley, 1990
5. MOTOGNA, S. – Metode de proiectare a compilatoarelor, Ed. Albastra, 2006
6. Schmidt,D.A. - Denotational semantics: a methodology for language development, William C. Brown, 1986.
7.Winskel,G. - The Formal Semantics of Programming Languages: an introduction, MIT Press, 1993
Assessment
The students will be asked to make a presentation of a paper from an additional reference and present it in public, during seminar hours. Also during the semester that have to work on a project that will implement one of the formal method presented in course for a mini-language they will specify. The final grade will be computed based on the following algorithm:
- seminar activity 30%
- project 40%
- final exam 40%
Foe academic year 2008-2009, see
http://cs.ubbcluj.ro/~motogna/FormalModels.html
Links: Syllabus for all subjects
Romanian version for this subject
Rtf format for this subject