-
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... -
Boltzmann samplers for random generation of lambda terms
Randomly generating structured objects is important in testing and optimizing functional programs, whereas generating random $'l$-terms is more specifically needed for... -
A semantics and a syntax for ordinal notations and hierarchies
Rapport interne. -
A CPS-semantics for a typed lambda-calculus of exception handling with fixed-...
Colloque avec actes et comité de lecture. -
$\rho$-Calculus. Its Syntax and Basic Properties
Rapport interne. -
A confluence Result for a Typed lambda-Calculus of Exception Handling with Fi...
Colloque avec actes et comité de lecture.
