Faculty of Science

Objectives

To introduce the student to a number of approaches in formally defining the semantics of programs and programming languages.

Contents

Various operational semantics: Floyd’s, Hoare's logic; partial/total correctness; Lattices and domains; fixed-point theorems and fixed point semantics; Algebraic semantics; Denotational semantics and its use in describing programming language constructs; Recursion and specification of semantics; Data types; Introductory notions on lambda-calculus and typed-lambda calculus; Introductory overview of process semantics: CSP, CCS, process algebras, coalgebras; Mention notions in: category theory; model-checking; Applications in: programming language design; proof of program properties; formal specifications; etc.; correctness, verification issues; theoretical foundations of functional languages.