Lambda-calculus and formal language theory
Résumé
Formal and symbolic approaches have offered computer science many
application fields. The rich and fruitful connection between logic,
automata and algebra is one such approach. It has been used to model
natural languages as well as in program verification. In the
mathematics of language it is able to model phenomena ranging from
syntax to phonology while in verification it gives model checking
algorithms to a wide family of programs.
This thesis extends this approach to simply typed lambda-calculus by
providing a natural extension of recognizability to programs that
are representable by simply typed terms. This notion is then applied
to both the mathematics of language and program verification. In
the case of the mathematics of language, it is used to generalize
parsing algorithms and to propose high-level methods to describe
languages. Concerning program verification, it is used to describe
methods for verifying the behavioral properties of higher-order
programs. In both cases, the link that is drawn between finite state
methods and denotational semantics provide the means to mix powerful
tools coming from the two worlds.
Loading...