-
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) -
Advances in the Logical Representation of Lexical Semantics
International audience -
Counting and generating lambda terms
International audience -
A Framework for Defining Logical Frameworks
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known... -
An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus.
11 pages. A preliminary version appeared as Research Report IAC CNR Roma , N.57 (11/2004), november 2004. -
(HO)RPO Revisited
The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used... -
Call-by-value non-determinism in a linear logic type discipline
International audience
