Benjamin Leperchey

Préféreriez-vous la version française de cette page ?

I was a PhD student in the PPS team.

Contact

As any member of PPS, my e-mail address is Surname.Name@pps.jussieu.fr.

Thesis

See this page.

Research

I was working on the semantics of programming languages, especially those of functional languages. I have been working of relative definability, and models for the length of computation. Some papers have been published:

• Relative Definability and Models of Unary PCF, with Antonio Bucciarelli and 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, with 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, with 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.