Ivan Scagnetto

LPAR Conference 2018 Conference Paper

The involutions-as-principal types/application-as-unification Analogy

• Alberto Ciaffaglione
• Furio Honsell
• Marina Lenisa
• Ivan Scagnetto

In 2005, S. Abramsky introduced various universal models of computation based on Affine Combinatory Logic, consisting of partial involutions over a suitable formal language of moves, in order to discuss reversible computation in a game-theoretic setting. We investigate Abramsky’s models from the point of view of the model theory of λ-calculus, focusing on the purely linear and affine fragments of Abramsky’s Combinatory Algebras. Our approach stems from realizing a structural analogy, which had not been hitherto pointed out in the literature, between the partial involution interpreting a combinator and the principal type of that term, with respect to a simple types discipline for λ-calculus. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction (GoI). Our approach provides immediately an answer to the open problem, raised by Abram- sky, of characterising those finitely describable partial involutions which are denotations of combinators, in the purely affine fragment. We prove also that the (purely) linear combinatory algebra of partial involutions is a (purely) linear λ-algebra, albeit not a combinatory model, while the (purely) affine combinatory algebra is not. In order to check the complex equations involved in the definition of affine λ-algebra, we implement in Erlang the compilation of λ-terms as involutions, and their execution.

LFMTP Workshop 2015 Workshop Paper

Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks

• Furio Honsell
• Luigi Liquori
• Petar Maksimovic 0001
• Ivan Scagnetto

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. Such calls are the basic tool for gluing together diverse Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the CMU School. The first system, CLLFP, is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLFP? , features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value lambda-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms.

TCS Journal 2015 Journal Article

Mechanizing type environments in weak HOAS

• Alberto Ciaffaglione
• Ivan Scagnetto

We provide a paradigmatic case study, about the formalization of System F <: 's type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F <: 's metatheory, on the other hand we address the equivalence of the two approaches internally to Coq.

LFMTP Workshop 2014 Conference Paper

Internal Adequacy of Bookkeeping in Coq

• Alberto Ciaffaglione
• Ivan Scagnetto

We focus on a common problem encountered in encoding and formally reasoning about a wide range of formal systems, namely, the representation of a typing environment. In particular, we apply the bookkeeping technique to a well-known case study (i.e., System F<:'s type language), proving in Coq an internal correspondence with a more standard representation of the typing environment as a list of pairs. In order to keep the signature readable and concise, we make use of higher-order abstract syntax (HOAS), which allows us to deal smoothly with the representation of the universal binder of System F<: type language.

IS Journal 2010 Journal Article

The Context-Aware Browser

• Paolo Coppola
• Vincenzo Della Mea
• Luca Di Gaspero
• Davide Menegon
• Danny Mischis
• Stefano Mizzaro
• Ivan Scagnetto
• Luca Vassena

The typical scenario of a user seeking information on the Web requires significant effort to get the desired information. In a world where information is essential, it can be crucial for users to get the desired information quickly even when they are away from their desktop computers. The Context-Aware Browser for mobile devices senses the surrounding environment, infers the user's current context, and proactively searches for and activates relevant Web documents and applications.

IS Journal 2009 Journal Article

Context-Aware Browser

• Paolo Coppola
• Vincenzo Della Mea
• Luca Di Gaspero
• Davide Menegon
• Danny Mischis
• Stefano Mizzaro
• Ivan Scagnetto
• Luca Vassena

LPAR Conference 2008 Conference Paper

A Conditional Logical Framework

• Furio Honsell
• Marina Lenisa
• Luigi Liquori
• Ivan Scagnetto

Abstract The Conditional Logical Framework LF K is a variant of the Harper-Honsell-Plotkin’s Edinburgh Logical Framemork LF. It features a generalized form of λ -abstraction where β -reductions fire under the condition that the argument satisfies a logical predicate. The key idea is that the type system memorizes under what conditions and where reductions have yet to fire. Different notions of β -reductions corresponding to different predicates can be combined in LF K. The framework LF K subsumes, by simple instantiation, LF (in fact, it is also a subsystem of LF!), as well as a large class of new generalized conditional λ -calculi. These are appropriate to deal smoothly with the side-conditions of both Hilbert and Natural Deduction presentations of Modal Logics. We investigate and characterize the metatheoretical properties of the calculus underpinning LF K, such as subject reduction, confluence, strong normalization.

ECAI Conference 2008 Conference Paper

AI on the Move: Exploiting AI Techniques for Context Inference on Mobile Devices

• Adolfo Bulfoni
• Paolo Coppola 0001
• Vincenzo Della Mea
• Luca Di Gaspero
• Danny Mischis
• Stefano Mizzaro
• Ivan Scagnetto
• Luca Vassena

Context aware computing is a computational paradigm that has faced a rapid growth in the last few years, especially in the field of mobile devices. One of the promises of context-awareness in this field is the possibility of automatically adapting the functioning mode of mobile devices to the environment and the current situation the user is in, with the aim of improving both their efficiency (using the scarce resources in a more efficient way) and effectiveness (providing better services to the user). We propose a novel approach for providing a basic infrastructure for context-aware applications on mobile devices, in which AI techniques (namely a principled combination of rule-based systems, Bayesian networks, and ontologies) are applied to context inference. The aim is to devise a general inferential framework to easier the development of context-aware applications by integrating the information coming from physical and logical sensors (e. g. , position, agenda) and reasoning about this information in order to infer new and more abstract contexts. In previous contextaware applications, most researches focused almost exclusively on time and/or location and other few data, while the same contexts inference was limited to preconceived values. Our approach differs from previous works since we do not focus on particular contextual values, but rather we have developed an architecture where managed contexts can be easily replaced by new contexts, depending on the different needs. Moreover, the inferential infrastructure we designed is able to work in a more general way and can be easily adapted to different models of applications distribution. We show some concrete examples of applications built upon the inferential infrastructure and we discuss its strengths and limitations.

TCS Journal 2001 Journal Article

π-calculus in (Co)inductive-type theory

• Furio Honsell
• Marino Miculan
• Ivan Scagnetto

We present a large and we think also significant case study in computer assisted formal reasoning. We start by giving a higher-order abstract syntax encoding of π-calculus in the higher-order inductive/coinductive-type theories CIC and CC (Co)Ind. This encoding gives rise to a full-fledged proof editor/proof assistant for the π-calculus, once we embed it in Coq, an interactive proof-development environment for CC (Co)Ind. Using this computerized assistant we prove formally a substantial chapter of the theory of strong late bisimilarity, which amounts essentially to Section 2 of A calculus of mobile processes by Milner, Parrow, and Walker. This task is greatly simplified by the use of higher-order syntax. In fact, not only we can delegate conveniently to the metalanguage α-conversion and substitution, but, introducing a suitable axiomatization of the theory of contexts, we can accommodate also the machinery for generating new names. The axiomatization we introduce is quite general and should be easily portable to other formalizations based on higher-order syntax. The use of coinductive types and corresponding tactics allows to give alternative, and possibly more natural, proofs of many properties of strong late bisimilarity, w. r. t. those originally given by Milner, Parrow, and Walker.