25 citations · 40 across the 7 of their papers we have counts for
7 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…
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Dale Miller, Ivan Scagnetto
This volume contains a selection of papers presented at LFMTP 2019, the 14th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on J…
Mobile Information Retrieval
Fabio Crestani, Stefano Mizzaro, Ivan Scagnetto
Mobile Information Retrieval (Mobile IR) is a relatively recent branch of Information Retrieval (IR) that is concerned with enabling users to carry out, using a mobile device, all…
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…
: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
Furio Honsell, Luigi Liquori, Petar Maksimovic +1
We extend the constructive dependent type theory of the Logical Framework with monadic, dependent type constructors indexed with predicates over judgements, called Lo…
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
Furio Honsell, Luigi Liquori, Petar Maksimović +1
We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle.…