Frédéric Lang's PhD



The thesis addresses the issue of defining models to implement the beta-reduction in the lambda-calculus. We focus especially on two kinds of models: explicit substitution calculi, and interaction nets.

  • Explicit substitution calculi are studied in several contexts. On the one hand, they are studied in the context of automatic provers, where it is interesting to have a calculus which is both confluent on terms with first-order variables and preserving strong normalization. These properties would allow for the representation of incomplete proofs. We discuss these properties, and give important contributions to an open problem in this field. On the other hand, explicit substitution calculi are applied to functional programming and weak reduction which is its fundamental concept. It is then essential to have tools which can express the sharing provided by implementations, particularly for lazy languages. To illustrate this, we give a very precise and formal proof of the correctness of KP, an abstract machine for lazy reduction of the lambda-calculus, using a calculus of explicit substitution and global adresses, namely lambda-sigma-w-a. We then propose an optimization for this machine.
  • Interaction nets are usually associated to optimal reduction à la Lévy, as described by Lamping's algorithm. However, this algorithm is known as rather complex. We study in our thesis a reducer based on some ideas due to Lamping, but leaving out some constraints introduced for optimality. Thus, we obtain a non optimal algorithm that we compare to Lamping's algorithm (implementation of Asperti) and KP. The results show as expected that our algorithm provides quite a good amount of sharing, without the bureaucracy that one finds in optimal interpreters.

 Download My thesis in french, postscript formatted, gzip compressed, is here.


Last updated: 2022/08/25 15:04:16