Course details

Programming Language Semantics

SPJ Acad. year 2012/2013 Winter semester 3 credits

Current academic year

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

Hruška Tomáš, prof. Ing., CSc. (DIFS)

Language of instruction

Czech

Completion

Examination

Time span

  • 26 hrs lectures

Department

Department of Information Systems (UIFS)

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

  1. History of programming languages construction development.
  2. Kinds of syntax and semantic definition.
  3. Basics of non-typed lambda calculus.
  4. Expresssion notation, evaluation.
  5. Recursive functions formal semantics.
  6. Name spaces and type checking.
  7. Data types simple and structured, type equivalence, polymorphism.
  8. Denotational semantics.
  9. Floyd-Hoare logic and its use for program correcntess proving.
  10. Axiomatic semantics and program correctness proving.
  11. Subroutine calling and parameter passing.
  12. Object-oriented programming.
  13. Functional programming, logic programming.

Progress assessment

Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.

Controlled instruction

Mid-term test.

Back to top