Faculty of Information Technology, BUT

Course details

Programming Languages

PRJ Acad. year 2004/2005 Summer semester 6 credits

Types of semantic programming languages semantic definition: denotational, operational and axiomatic. Lambda calculus a its using for the denational semantic. Formal definition of basic types, structures a constructions using denotational semantic. Axiomatic semantic and its using for program correctnes proving. Examples of axiomatic definitions. The semantic of languages for functional and logic programming. Basics of object-oriented programming.


Language of instruction



Credit+Examination (written)

Time span

39 hrs lectures, 12 hrs exercises, 14 hrs projects

Assessment points

50 exam, 20 half-term test, 30 projects



Subject specific learning outcomes and competences

Ability to formally define programming languages sematic a to use this definition in praxis. Ability and practical using of the program correctnes proving.

Learning objectives

To obtain theoretical foundations of the programming languages construction semantic definition. To obtain the ability to define this semantic and to use this definiction in praxis. To obtain an overview about basic models of programming languages.

Prerequisite kwnowledge and skills

theoretical informatics, formal languages

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

Fundamental literature

  • Gordon,J.C.: Programming Language Theory and its Implementation, Prentice Hall - Series in Computer Science, Prentice Hall New York 1988, 255 p., ISBN 0-13-730409-9
  • Sebesta,R.,W.: Concepts of Programming Languages, Addison Wesley, Massachusetts 1999, 670 p., 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.
  • Name spaces and type checking.
  • Data types simple and structured, type equivalence, polymorphism.
  • Denotational semantics.
  • Floyd-Hoare logic.
  • Axiomatic semantics and program proving.
  • Subroutine calling and parameter passing.
  • Object-oriented programming.
  • Functional programming, logic programming.

Syllabus of numerical exercises

  • Basic constructions and operation of lambda calculus.
  • Simple types reprezentation in lambda calculus.
  • Structured types reprezentation in lambda calculus.
  • Denotational semantics of a simple language.
  • Basics of Floyd-Hoare logic.
  • Program proving.

Syllabus - others, projects and individual work of students

  • Realization of semantic part of various simple languages compilers. In combination with the project from the course Compiler design.

Progress assessment

Half semester test. Continuous checking of the project solution by the supervisor.

Controlled instruction

Presence at the numerical exercises. 14-days cyclus. it is possible to present extraordinary in the other week.

Exam prerequisites

At least half of points obtainable during the semester (tests a project), i.e. 25 points.
Back to top