Learning outcomes in more details

Prerequisites

The aim of this chapter is to introduce the mathematical concepts needed to assimilate the main concepts covered by the module. At the end of this chapter:

• The student has been reminded of the various notions related to programming languages and programming paradigms.
• The student is able to read the definition of a formal system.
• The student is able to write proofs in a given formal system.
• The student has studied fixed point theory.

Lambda-Calculus and Typed Lambda-Calculus

At the end of this chapter, the student will be able to:

• Define, introduce and explain the lambda calculus
• Evaluate expressions in the Lambda-Calculus (particularly beta-reduction).
• Illustrate the notion of calculability in Lambda-Calculus.
• Write programs in Lambda-Calculus.

Classical and Intuitionistic Logic

At the end of this chapter, the student will be able to:

• Introduce intuitionistic logic.
• Distinguish between and compare classical logic and intuitionistic logic.
• Write proofs in intuitionistic logic.

Fromal semantics

The aim of this chapter is to present the theoretical notions related to the formal semantics of programming languages. Thus, at the end of this chapter, the student will be able to:

• Define the concept of Formal Semantics.
• Explain the objectives and contribution of Formal Semantics.
• Name, describe and illustrate the different types of formal semantics.

Formal expression of semantics

This chapter covers the practical part of the theoretical notions presented in the previous chapter. At the end of this chapter, the student will be able to:

• Read the formal specification of a programming language.
• Write program proofs using formal semantics.
• Adapt and modify a specification to change the characteristics of a programming language.
• Write proofs in a proof environment.