Benjamin Leperchey

Would you rather read an english version of this page?

J'ai été pendant trois ans doctorant dans le laboratoire PPS, sous la direction d'Antonio Bucciarelli. Aujourd'hui, je passe quand même nettement plus de temps sur mon nouveau lieu de travail, qui n'a plus grand chose à voir avec la recherche en informatique (ni avec le recherche tout court, d'aileurs).

Coordonnées

Comme tous membre de PPS qui se respecte, on peut me joindre à l'adresse Prénom.Nom@pps.jussieu.fr.

Soutenance

Voyez cette page pour des informations et une version preliminaire du memoire.

Travaux de recherche

Je travaillais sur la sémantique des langages de programmation, et plus particulièrement des langages fonctionnels. J'ai travaillé sur la définissabilité relative, et sur les modèles du temps de calcul. Parmi les diverses choses que j'ai écrites, on trouve des publications:

• Relative Definability and Models of Unary PCF, avec Antonio Bucciarelli et Vincent Padovani, TLCA 2003.
  We show that the poset of degrees of relative definability in the Scott model of Unary PCF is non trivial, and that, nevertheless, the hierarchy of order extensional models of the language is reduced to a bottom element (the fully abstract model) and a top one (the Scott model itself).
• Hypergraphs and degrees of parallelism: a completeness result, avec Antonio Bucciarelli, FOSSACS 2004.
  In order to study relative PCF-definability of boolean functions, we associate a hypergraph $H_f$ to any boolean function $f$. We introduce the notion of timed hypergraph morphism and show that it is:
  - Sound: if there exists a timed morphism from $H_f$ to $H_g$ then $f$ is PCF-definable relatively to $g$.
  - Complete for subsequential functions: if $f$ is PCF-definable relatively to $g$, and $g$ is subsequential, then there exists a timed morphism from $H_f$ to $H_g$.
  We show that the problem of deciding the existence of a timed morphism between two given hypergraphs is NP-complete.
• Relational Reasoning in a Nominal Semantics for Storage, avec Nick Benton, TLCA 2005.
  We give a monadic semantics in the category of FM-cpos to a higher-order CBV language with recursion and dynamically allocated mutable references that may store both ground data and the addresses of other references, but not functions. This model is adequate, though far from fully abstract. We then develop a relational reasoning principle over the denotational model, and show how it may be used to establish various contextual equivalences involving allocation and encapsulation of store.

• Time and Games.
  We add the notion of time to denotational models of the lambda-calculus. The denotation is no longer constant through reduction, but rather decreases with respect to an appropriate order. Categorically, we use a monad over a cartesian category, an order over the morphisms of the Kleisli category, and a Galois connection to model the beta-reduction. We define a generic monad (time as a resource), and an instance of this construction in game semantics, where our timings are precise enough to simulate parallelism through interleaving.
• Call-By-Name, Call-By-Value, and Time.
  We build denotational models for the call-by-name and call-by-value versions of a simply typed lambda calculus with recursion, and show that they are adequate: the denotation of a closed term of base type represents exactly the number of reduction steps. We achieve this in a very generic way, using monads to propagate the information about the number of steps. The denotations in the Kleisli category are then straightforward.