UP | HOME

Research Activity

Table of Contents

Research interests

My main interests are in programming languages, from a semantic perspective. Most of my research activities have dealt with

  • the operational semantics of programming languages, and its relationship to other semantics and to machine implementations,
  • the verification of programs,
  • the synthesis of programs.

I try to adopt formal methods to solve the problems I tackle. For instance, as I have often met infinite objects, like infinite computations or recursive definitions, I have studied some logical and mathematical foundations that allows these infinite objects:

  • to be defined by using recursive equations,
  • to be reasoned upon by resorting to coinduction.

I also began to use COQ, a proof assistant. In other words, the proofs I develop becomes machine-checked.

I have especially applied these formal techniques to security problems.

  • Mobile code security : when executing mobile code, how to protect the host system from mobile code by controlling accesses to local resources and information flows between the mobile code and the host system.
  • Availability: how to ensure the availability of a resource shared by different users.
  • Reference monitors: how to formalize the actions of a reference monitor modeled as a transducer.

Introductory explanation

Semantics deals with the following question: what does a program mean?

The answer depends on the level you consider.

At the user level, a program generally is a model of some artifacts, for instance the different flows in an information system. The problem is here to find the good abstractions, in other words the abstractions that are well suited to users, being close to artifacts. Nowadays, there is a strong trend to use abstract models in software engineering: model-driven engineering resorts to domain-specific languages in order to reduce the gap between programs and artifacts that are modeled.

At the implementer level, a program is not only a model but also a command of the machine executing the code. The problem is here to understand the operational meaning of the program in order to correctly command the machine. What is a machine? The machine may be virtual. At the most abstract level, it is implemented in the human spirit. Although this machine generally remains informal and intuitive, it may also be formalized in elegant and effective ways. Operational semantics becomes close to logic. At a more concrete level, it is implemented in a computer, either by software or by hardware: see for instance the Java virtual machine, a program that executes Java programs, and a processor, a piece of hardware that executes binary programs.

See also

Last Updated 2015-04-17T08:45+0200. Comments or questions: Send a mail.