10 citations · 32 across the 10 of their papers we have counts for
11 papers
Sensible Intersection Type Theories
Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini +1
Finitary/static semantics in the form of intersection type assignments have become a paradigm for analysing the fine structure of all sorts of lambda-models. The key step is the co…
Principal Types as Partial Involutions
Furio Honsell, Marina Lenisa, Ivan Scagnetto
We show that the principal types of the closed terms of the affine fragment of -calculus, with respect to a simple type discipline, are structurally isomorphic to their interpre…
On Quantitative Algebraic Higher-Order Theories
Ugo Dal Lago, Furio Honsell, Marina Lenisa +1
We explore the possibility of extending Mardare et al. quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all,…
A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio +2
The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus…
A prototype-based approach to object reclassification
Ciaffaglione Alberto, Di Gianantonio Pietro, Honsell Furio +1
We investigate, in the context of functional prototype-based lan- guages, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by…
Lambda-calculus and Reversible Automatic Combinators
Alberto Ciaffaglione, Furio Honsell, Marina Lenisa +1
In 2005, Abramsky introduced various linear/affine combinatory algebras of partial involutions over a suitable formal language, to discuss reversible computation in a game-theoreti…