-
Principal Types as Partial Involutions
Authors:
Furio Honsell,
Marina Lenisa,
Ivan Scagnetto
Abstract:
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 interpretations, as partial involutions, in a natural Geometry of Interaction model à la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of linear application arising in Geometry of Interaction,…
▽ More
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 interpretations, as partial involutions, in a natural Geometry of Interaction model à la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of linear application arising in Geometry of Interaction, simply as the resolution between principal types using an alternate unification algorithm. As a consequence, we provide an answer, for the purely affine fragment, to the open problem raised by Abramsky of characterising those partial involutions which are denotations of combinatory terms.
△ Less
Submitted 11 February, 2024;
originally announced February 2024.
-
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Authors:
Dale Miller,
Ivan Scagnetto
Abstract:
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 June 22, 2019, in Vancouver, Canada. The workshop was affiliated with the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
Logical frameworks and meta-languages form a common substrate for re…
▽ More
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 June 22, 2019, in Vancouver, Canada. The workshop was affiliated with the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects im**ing on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
△ Less
Submitted 19 October, 2019;
originally announced October 2019.
-
Mobile Information Retrieval
Authors:
Fabio Crestani,
Stefano Mizzaro,
Ivan Scagnetto
Abstract:
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 the classical IR operations that they were used to carry out on a desktop. This includes finding content available on local repositories or on the web in response to a user query, interacting with the system in an explic…
▽ More
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 the classical IR operations that they were used to carry out on a desktop. This includes finding content available on local repositories or on the web in response to a user query, interacting with the system in an explicit or implicit way, reformulate the query and/or visualise the content of the retrieved documents, as well as providing relevance judgments to improve the retrieval process.
This book is structured as follows. Chapter 2 provides a very brief overview of IR and of Mobile IR, briefly outlining what in Mobile IR is different from IR. Chapter 3 provides the foundations of Mobile IR, looking at the characteristics of mobile devices and what they bring to IR, but also looking at how the concept of relevance changed from standard IR to Mobile IR. Chapter 4 presents an overview of the document collections that are searchable by a Mobile IR system, and that are somehow different from classical IR ones; available for experimentation, including collections of data that have become complementary to Mobile IR. Similarly, Chapter 5 reviews mobile information needs studies and users log analysis. Chapter 6 reviews studies aimed at adapting and improving the users interface to the needs of Mobile IR. Chapter 7, instead, reviews work on context awareness, which studies the many aspects of the user context that Mobile IR employs. Chapter 8 reviews some of evaluation work done in Mobile IR, highlighting the distinctions with classical IR from the perspectives of two main IR evaluation methodologies: users studies and test collections. Finally, Chapter 9 reports the conclusions of this review, highlighting briefly some trends in Mobile IR that we believe will drive research in the next few years.
△ Less
Submitted 5 February, 2019;
originally announced February 2019.
-
The Delta-framework
Authors:
Furio Honsell,
Luigi Liquori,
Claude Stolze,
Ivan Scagnetto
Abstract:
We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contr…
▽ More
We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subty**, LF-Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF-Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.
△ Less
Submitted 13 August, 2018;
originally announced August 2018.
-
Lambda-calculus and Reversible Automatic Combinators
Authors:
Alberto Ciaffaglione,
Furio Honsell,
Marina Lenisa,
Ivan Scagnetto
Abstract:
In 2005, Abramsky introduced various linear/affine combinatory algebras of partial involutions over a suitable formal language, to discuss reversible computation in a game-theoretic setting. These algebras arise as instances of the general paradigm explored by Haghverdi (Abramsky's Programme), which amounts to defining a lambda-algebra starting from a GoI Situation in a traced symmetric monoidal c…
▽ More
In 2005, Abramsky introduced various linear/affine combinatory algebras of partial involutions over a suitable formal language, to discuss reversible computation in a game-theoretic setting. These algebras arise as instances of the general paradigm explored by Haghverdi (Abramsky's Programme), which amounts to defining a lambda-algebra starting from a GoI Situation in a traced symmetric monoidal category. We investigate this construction from the point of view of the model theory of lambda-calculus. We focus on the strictly linear and affine parts of Abramsky's Affine Combinatory Algebras, sketching how to encompass the full algebra. The gist of our approach is that the GoI interpretation of a term based on involutions is dual to the principal type of the term, w.r.t. the type discipline for a linear/affine lambda-calculus. In the general case the type discipline and the calculus need to be extended, resp., with intersection, !-types, and !-abstractions. Our analysis unveils three conceptually independent, but ultimately equivalent, accounts of application in the lambda-calculus: beta-reduction, the GoI application of involutions based on symmetric feedback (Girard's Execution Formula), and unification of principal types. Thus we provide an answer, in the strictly affine case, to the question raised in [1] of characterising the partial involutions arising from bi-orthogonal pattern matching automata, which are denotations of affine combinators, and we point to the answer to the full question. Furthermore, we prove that the strictly linear combinatory algebra of partial involutions is a strictly linear lambda-algebra, albeit not a combinatory model, while both the strictly affine combinatory algebra and the full affine combinatory algebra are not. To check all the equations involved in the definition of affine lambda-algebra, we implement in Erlang application of involutions.
△ Less
Submitted 30 August, 2018; v1 submitted 18 June, 2018;
originally announced June 2018.
-
$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
Authors:
Furio Honsell,
Luigi Liquori,
Petar Maksimovic,
Ivan Scagnetto
Abstract:
We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delega…
▽ More
We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,σ}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,σ}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,σ}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $λ$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.
△ Less
Submitted 5 July, 2017; v1 submitted 23 February, 2017;
originally announced February 2017.
-
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
Authors:
Furio Honsell,
Luigi Liquori,
Petar Maksimović,
Ivan Scagnetto
Abstract:
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…
▽ More
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.
△ Less
Submitted 29 July, 2015;
originally announced July 2015.
-
A weak HOAS approach to the POPLmark Challenge
Authors:
Alberto Ciaffaglione,
Ivan Scagnetto
Abstract:
Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language of pure System F<: within Coq, a proof assistant based on the Calculus of Inductive Constructions.
Our encoding allows us to accomplish the proof of the transitivity property of algorithmic subty**, which is in fact…
▽ More
Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language of pure System F<: within Coq, a proof assistant based on the Calculus of Inductive Constructions.
Our encoding allows us to accomplish the proof of the transitivity property of algorithmic subty**, which is in fact the first of the three tasks stated by the POPLmark Challenge, a set of problems that capture the most critical issues in formalizing programming language metatheory.
△ Less
Submitted 29 March, 2013;
originally announced March 2013.
