8 citations · 13 across the 5 of their papers we have counts for
6 papers
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…
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…
Conway games, algebraically and coalgebraically
Furio Honsell, Marina Lenisa
Using coalgebraic methods, we extend Conway's theory of games to possibly non-terminating, i.e. non-wellfounded games (hypergames). We take the view that a play which goes on forev…
RPO, Second-order Contexts, and Lambda-calculus
Pietro Di Gianantonio, Furio Honsell, Marina Lenisa
First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possib…