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, 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 characterizing those partial involutions which are denotations of combinatory terms.

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 subtyping, 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.

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.

We present two extensions of theLFconstructive type theory featuring monadiclocks. A lock is a monadic type construct that captures the effect of anexternal call to an oracle. Such calls are the basic tool forplugging-inand gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in thecanonical styledeveloped by the ‘CMU School.’ The first system,CLLF𝒫, is the canonical version of the systemLLF𝒫, presented earlier by the authors. The second system,CLLF𝒫?, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms ofCLLF𝒫andCLLF𝒫?permit to factor out naturally the complexities arising from enforcing these ‘side conditions,’ which severely obscure standardLFencodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial.

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,\sigma}[\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,\sigma}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,\sigma}[\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 $\lambda$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory. Comment: Accepted for publication in LMCS

The LF P Framework is an extension of the Harper–Honsell–Plotkin's Edinburgh Logical Framework LF with external predicates , hence the name Open Logical Framework . This is accomplished by defining lock type constructors , which are a sort of ⋄ -modality constructors , releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i . e . via introduction , elimination and equality rules . Using LF P , one can factor out the complexity of encoding specific features of logical systems, which would otherwise be awkwardly encoded in LF, e . g . side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non-commutative Linear Logic . The idea of LF P is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincaré Principle or Deduction Modulo . Indeed such paradigms can be adequately formalized in LF P . We investigate and characterize the meta-theoretical properties of the calculus underpinning LF P : strong normalization, confluence and subject reduction. This latter property holds under the assumption that the predicates are well-behaved , i . e . closed under weakening, permutation , substitution and reduction in the arguments. Moreover, we provide a canonical presentation of LF P , based on a suitable extension of the notion of βη - long normal form , allowing for smooth formulations of adequacy statements.

We propose a novel approach to address the problem of the recognition of important locations. Our method is organised in two phases: first, a set of candidate stay points is identified by exploiting some state-of-the-art algorithms to filter the GPS-logs, then, the candidate stay points are mapped onto a feature space having as dimensions the area underlying the stay point, its intensity (the time spent in a location) and its frequency (the number of total visits). We conjecture that the features space allows to model aspects/measures that are more semantically related to users and better suited to reason about their similarities and differences than, e.g., Latitude, longitude, and timestamp. An experimental evaluation on the GeoLife public dataset confirms the effectiveness of our approach.

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.

The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on functor categories . By means of a suitable notion of forcing , we prove that this model validates Classical Higher Order Logic, the Theory of Contexts, and also (parametrised) structural induction and recursion principles over contexts. Our approach, which we present in full detail, should also be useful for reasoning on other models based on functor categories. Moreover, the construction could also be adopted, and possibly generalized, for validating other theories of names and binders.

We investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders.First, we introduce typed binding signatures and develop a theory of typed abstract syntax with binders. Each signature is associated to a category of "presentation" models, where the language of the typed signature is the initial model.At the semantic level, types can be given also a computational meaning in a (possibly different) semantic category. We observe that in general, semantic aspects of terms and variables can be reflected in the presentation category by means of an adjunction. Therefore, the category of presentation models is expressive enough to represent both the syntactic and the semantic aspects of languages.We introduce then a metalogical system, inspired by the internal languages of the presentation category, which can be used for reasoning on both the syntax and the semantics of languages. This system is composed by a core equational logic tailored for reasoning on the syntactic aspects; when a specific semantics is chosen, the system can be modularly extended with further "semantic" notions, as needed.

A relevant issue for any Virtual Environment (VE) is the navigational support provided to users who are exploring it. Semitransparency is sometimes exploited as a means to see through occluding surfaces with the aim of improving user navigation abilities and awareness of the VE structure. Designers who make this choice assume that it is useful, especially in the case of VEs with many levels of occluding surfaces, e.g. virtual buildings or cities. This paper is devoted to investigate this assumption with a proper experimental evaluation on users. First, we discuss possible ways for improving navigation, and focus on implementation choices for semitransparency as a navigation aid. Then, we present and discuss the experimental evaluation we carried out. We compared subjects' performance in three conditions: local exploitation of semitransparency inside the VE, a more global exploitation provided by a bird's-eye-view, and a control condition where neither of the two features was available.