-
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... -
Complexité Implicite de Lambda-Calculs Concurrents
Controlling the resource consumption of programs is crucial: besides performance reasons, it has many applications in the field of computer security where e.g. mobile... -
Elementary Linear Logic Revisited for Polynomial Time and an Exponential Time...
International audience -
Light logics and optimal reduction: Completeness and complexity
International audience -
Type-theoretical natural language semantics: on the system F for meaning asse...
International audience -
Resource control and strong normalisation
We introduce the \emph{resource control cube}, a system consisting of eight intuitionistic lambda calculi with either implicit or explicit control of resources and... -
A journey through resource control lambda calculi and explicit substitution u...
In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda... -
Counting and generating lambda terms
Lambda calculus is the basis of functional programming and higher order proof assistants. However, little is known about combinatorial properties of lambda terms, in... -
Type inference for light affine logic via constraints on words.
This dataset has no description
-
Checking polynomial time complexity with types.
This dataset has no description
-
A feasible algorithm for typing in Elementary Affine Logic.
We give a new type inference algorithm for typing lambda-terms in Elementary Affine Logic (EAL), which is motivated by applications to complexity and optimal... -
Soft lambda-calculus: a language for polynomial time computation.
Version préliminaire (longue) disponible comme ccsd-00012751 (2003)
