Abstract
After six lectures devoted to imperative languages, where the basic operation is the modification of a state, the seventh lecture has changed paradigm and turned the spotlight on functional languages, where the basic operations are the abstraction and application of functions, as in lambda-calculus. To facilitate programming, functional languages add a reduction strategy and primitive data types to lambda-calculus. They are given operational semantics either in the form of context-sensitive reductions, or in the natural style. We have mechanized the syntax and semantics of a small functional language in Coq, called " FUN ", with the only difficulty being the absence of alpha-conversion, restricting us to the weak evaluation of closed programs.
When a language offers multiple data types, such as functions and booleans in FUN, absurd programs appear, such as true false (applying the boolean true as if it were a function). Typing is a way of rejecting such nonsensical programs, either dynamically (at runtime) or statically (by static analysis). We've added a system of static simple types to the FUN language, similar to Church's simply typed lambda-calculus. To demonstrate the safety of a type system, i.e. the fact that no well-typed program is absurd, several techniques exist depending on the style of semantics used : denotational, natural, or reduction. In the latter case, the demonstration is based on two properties linking typing and reductions : preservation (of typing by a reduction) and progression (a well-typed program is a value or reduces).
The lecture and the mechanization have so far followed an " extrinsic " approach to typing, where the type system applies like a filter on an untyped language. An " intrinsic " approach is also possible, where the abstract syntax and semantics of the language are defined only for well-typed terms. This requires the abstract syntax to be defined using dependent types, or at least generalized algebraic types (GADT). The advantage of this " intrinsic " approach is that it is possible to define a denotational semantics for the language which, by construction, guarantees not only typing safety but also standardization (all well-typed programs terminate). Extending this approach to rich languages and type systems is still an active research topic.
