We have seen in this lecture that functional programming has very deep mathematical logic foundations. These are the foundations that make reasoning about functional programming so easy and so powerful.
| We may also
think to put everything together. We may imagine a system where we have
simple types, high order types, type constructors and dependent types. This
system, which is denoted by LC, is known as Calculus of Constructions. It
is the basis of the formal system Coq that will be presented later in this
course. We have seen in this lecture that functional programming has very deep mathematical logic foundations. These are the foundations that make reasoning about functional programming so easy and so powerful. |
|
