Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
Domeniul: Informatica
Programul de studii: Programare bazată pe componente - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MID1004	Formal Models in Programming Languages	

Semester	Hours: C+S+L	Category	Status	
2	2+1+0	speciality	compulsory	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
MOTOGNA Simona Claudia	Ph.D.	Assoc.Prof.	Programming  Languages and Methods	*			

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
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. 	

IV. Course contents
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 problem of semantic equivalence will be discussed.	

V. Bibliography
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	

VI. Thematic of didactic activities per weeks
1. Introduction – What is a formal method? Criteria for specifications. Specification methods [3,4]
2. Semantic analysis: Attribute grammars. [2,5]
3. L-attribute and S-attribute grammars. Attribute evaluator [2,5]
4. Manual methods [2,5]

Operational semantics:
5. Transition systems. The idea of structural operational semantics [3,7]
6. Transition semantics of a simple imperative language. Language design options. [3,7]
7. Rule-based inductive definitions and proofs [3,7]
8. Functions. Call-by-name and call-by-value function application, semantics and typing. [3,7]
9. Data. Semantics and typing for products, sums, records, references. [3,7]
10. Subtyping. Record subtyping and simple object encoding. [3,7]
11. Semantic equivalence. Semantic equivalence of phrases in a simple imperative language, including the congruence property. Examples of equivalence and non-equivalence. [3,7]

 Denotational semantics:
12. Introduction to lambda-calculus [4,6]
13. Denotational interpretation of an imperative language. [4,6]
14. Differences between operational and denotational semantics [4,6]	

VII. Didactic methods used
The course is based on the following methods: exposure, conversation, didactical proof, modeling. The seminar will focus on: algorithmization, discovery and case studies.	

VIII. 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	

IX. Additional references
1. GIANNINI, P. - LONGO, G.: Effectively given domains and lambda-calculus semantics, Information and Control, 62(1984) no. 1, pp. 36-63. 
2. HOARE, C.A.R. - LAUER, P.: Consistent and Complementary definitions of the semantics of programming languages, Acta Informatica, 1973 no.3, pp. 135-153. 
3. LONGO, G.: Set-Theoretical models of Lambda-Calculus: Theories, Expansions, Isomorphisms, Annals of Pure and Applied Logic, 1983 no.24, pp. 153-188. 

	Dean,							Chair head,

	Date,							Course responsible,
							Assoc.Prof. MOTOGNA Simona Claudia, Ph.D.