Course details
Programming Language Semantics
SPJ Acad. year 2013/2014 Winter semester 3 credits
Types of semantic programming languages semantic definition: denotational, operational and axiomatic. Lambda calculus and its use for the denotational semantic. Formal definition of basic types, structures a constructions using denotational semantic. Axiomatic semantic and its use for program correctness proving. Examples of axiomatic definitions. The semantic of languages for functional and logic programming.
Guarantor
Language of instruction
Completion
Time span
- 26 hrs lectures
Department
Subject specific learning outcomes and competences
Ability of formally defining programming languages sematic and using this definition in praxis. Ability and practical use of the program correctness proving.
Learning objectives
In-depth grasp of theoretical foundations of the programming languages construction semantic definition. Obtaining the ability to define this semantic and use this definition in praxis.
Prerequisite knowledge and skills
There are no prerequisites
Study literature
- Češka, M., Motyčková, L., Hruška, T.: Vyčíslitelnost a složitost, skriptum VUT Brno, Ediční středisko VUT Brno 1992, 217 str., ISBN 80-214-0441-8
- Gordon, J.C.: Programming Language Theory and its Implementation, Prentice Hall - Series in Computer Science, Prentice Hall New York 1988, 255 str., ISBN 0-13-730409-9
Fundamental literature
- Gordon, J.C.: Programming Language Theory and its Implementation, Prentice Hall - Series in Computer Science, Prentice Hall New York 1988, 255 str., ISBN 0-13-730409-9
- Sebesta, R.,W.: Concepts of Programming Languages, Addison Wesley, Massachusetts 1999, 670 str., ISBN 9-780201-385960
Syllabus of lectures
- History of programming languages construction development.
- Kinds of syntax and semantic definition.
- Basics of non-typed lambda calculus.
- Expresssion notation, evaluation.
- Recursive functions formal semantics.
- Name spaces and type checking.
- Data types simple and structured, type equivalence, polymorphism.
- Denotational semantics.
- Floyd-Hoare logic and its use for program correcntess proving.
- Axiomatic semantics and program correctness proving.
- Subroutine calling and parameter passing.
- Object-oriented programming.
- Functional programming, logic programming.
Progress assessment
Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.
Teaching methods and criteria
The course uses teaching methods in form of Lecture - 2 teaching hours per week.
Controlled instruction
Mid-term test.