Our treatment of programming language semantics will be mathematical. Just as in Formal Language Theory, there will be important theories and techniques. These will inform our design, implementation and use of programming languages.
We start with a simple fragment of mathematics that is needed in this course. I will present it in a way that brings out the computational content explicitly because there is a strong connection between this mathematics and the functional part of the programming language ML.In order to make the connection between mathematics and ML clear, we will present the mathematics using the concept of type rather than set as cantral. There is a long tradition of expressing the foundations of mathematics this way, going back to Russell, Church and others with modern contribution by de Bruijn and Martin-Löf. Most working mathematics is ordinarily presented in terms of types.
We start with atomic types and type constructors . Note that types are not connected to any expression nor any operation. We will learn this notation in dual way: Math. and ML, because of the similarity between programming language types and math. types.