-
Lambda-Calculus, Multiplicities and the pi-Calculus
In this paper we study the semantics of the $\lambda$-calculus induced by Milner's encoding into the $\pi$-calculus. We show that the resulting may testing preorder on... -
Decidability of All Minimal Models (Revised Version - 2012)
This unpublished note is an alternate, shorter (and hopefully more readable) proof of the decidability of all minimal models. The decidability follows from a proof of... -
Lazy functions and mobile processes
This paper continues the study of Milner's encoding of the lazy $\lambda$-calculus into the $\pi$-calculus \cite{Mil92}. The encoding is shown to give rise to a... -
The discriminating power of multiplicities in the $\lambda$-calculus
The $\lambda$-calculus with multiplicities is a refinement of the lazy $\lambda$-calculus where the argument in an application comes with a multiplicity, which is an... -
An explicit $Eta$ rewrite rule
Projet EURECA -
Asymptotically almost all $\lambda$-terms are strongly normalizing
We present quantitative analysis of various (syntactic and behavioral) properties of random $\lambda$-terms. Our main results are that asymptotically all the terms are... -
The Origins of lambda-calculus and term rewriting systems
We use origin functions to describe the notion of descendance and residuals in reduction systems such as the lambda-calculus and lineart term rewriting systems. We... -
A proposed classification of intelligent manufacturing systems using consiste...
A new classification of Intelligent Manufacturing Systems (IMS) based on consistency analysis is proposed. Through this approach, IMS can be initially classified into... -
Wide-coverage semantics for spatio-temporal reasoning
International audience -
A Generative Montagovian Lexicon for Polysemous Deverbal Nouns
Accepted for publication in the proceedings of 4th congress on Universal Logic --- Logic and linguistics workshop. Rio de Janeiro April 4-7 2013. -
Intersection Types with Subtyping by Means of Cut Elimination
International audience -
Resource control and strong normalisation (old version)
We introduce the resource control cube, a system consisting of eight intuitionistic lambda calculi with either implicit or explicit control of resources and with... -
Toward a geometric view on computations
We interpret Intersection Types as the closed sets of some Zariski topology on pure lambda-terms. In this view, the parallel or operator introduced by Boudol is the... -
A relational semantics for parallelism and non-determinism in a functional se...
International audience -
Resource Lambda-Calculus: the Differential Viewpoint
International audience -
Realizability and parametricity in Pure Type Systems
This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to... -
Toward a General Rewriting-Based Framework for Reducibility
Reducibility is a powerful proof method which applies to various properties of typed terms in different type systems. For strong normalization, different vari- ants...
