To show the organization of the course that includes this module, follow this link Course organization
The aim of the course is to present the theoretical basis of programming languages. A number of paradigmatic untyped and typed languages will be introduced. The entire course will focus on the concepts of operational semantics and type system. Formal techniques for verifying the behaviour of programs will be introduced.
(i) Mathematical induction over the natural numbers;
(ii) Structural induction;
(iii) Rule induction.
Big step and small step semantics for simple languages including
(i) Exp, Bool, languages for arithmetic and Boolean expressions
(ii) the imperative language of while commands While
(iii)the functional languages Fun and Lambda and simple variations on them; call-by-name and call-by-value semantics.
(i) Typing assignments for the languages Fun and Lambda
(ii) Progress and preservation.
(iii) For Lambda you should be familiar with the computational consequences of using types; in particular the need for explicit fixpoint operators.
|Carl A. Gunter||Semantics of Programming Languages||MIT Press||1992||0262570955|
|G. Winskel||The formal Semantics of Programming Languages||MIT Press||1993|
The exam consists of a written and oral test.
Strada le Grazie 15
VAT number 01541040232
Italian Fiscal Code 93009870234
© 2021 | Verona University | Credits