-
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 -
Counting Terms in the Binary Lambda Calculus
International audience -
Nested Deduction in Logical Foundations for Computation
This thesis investigates the use of deep inference formalisms as basis for a computational interpretation of proof systems, following the two main approaches:... -
A pragmatic reconstruction of Lambda-Prolog
International audience -
Böhm trees as higher-order recursion schemes
International audience -
The Heart of Intersection Type Assignment
This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types. The technique applied is to define...
