Arrow Research search

Author name cluster

Marina Lenisa

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

16 papers
2 author rows

Possible papers

16

FSCD Conference 2022 Conference Paper

On Quantitative Algebraic Higher-Order Theories

  • Ugo Dal Lago
  • Furio Honsell
  • Marina Lenisa
  • Paolo Pistone

We explore the possibility of extending Mardare et al. ’s quantitative algebras to the structures which naturally emerge from Combinatory Logic and the λ-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results clearly delineating to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.

LFMTP Workshop 2019 Workshop Paper

A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning

  • Fabio Alessi
  • Alberto Ciaffaglione
  • Pietro Di Gianantonio
  • Furio Honsell
  • Marina Lenisa

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 allowing for external evidence and for postponing, delegating, or factoring-out side conditions. In particular, LLFP allows for reducing the number of times a proof-irrelevant check is performed. In this paper we give a shallow, actually definitional, implementation of LLFP in Coq, i. e. we use Coq both as host framework and oracle for LLFP. This illuminates the principles underpinning the mechanism of Lock-types and also suggests how to possibly extend Coq with the features of LLFP. The derived proof editor is then put to use for developing case-studies on an emerging paradigm, both at logical and implementation level, which we call fast and loose reasoning following Danielsson et alii [6]. This paradigm trades off efficiency for correctness and amounts to postponing, or running in parallel, tedious or computationally demanding checks, until we are really sure that the intended goal can be achieved. Typical examples are branch-prediction in CPUs and optimistic concurrency control.

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.

TCS Journal 2015 Journal Article

Multigames and strategies, coalgebraically

  • Marina Lenisa

Coalgebraic games have been recently introduced as a generalization of Conway games and other notions of games arising in different contexts. Using coalgebraic methods, games can be viewed as elements of a final coalgebra for a suitable functor, and operations on games can be analyzed in terms of (generalized) coiteration schemata. Coalgebraic games are sequential in nature, i. e. , at each step either the Left (L) or the Right (R) player moves (global polarization); moreover, only a single move can be performed at each step. Recently, in the context of Game Semantics, concurrent games have been introduced, where global polarization is abandoned, and multiple moves are allowed. In this paper, we introduce coalgebraic multigames, which are situated half-way between traditional sequential games and concurrent games: global polarization is still present, however multiple moves are possible at each step, i. e. , a team of L/R players moves in parallel. Coalgebraic operations, such as sum and negation, can be naturally defined on multigames. Interestingly, sum on coalgebraic multigames turns out to be related to Conway's selective sum on games, rather than the usual (sequential) disjoint sum. Selective sum has a parallel nature, in that at each step the current player performs a move in at least one component of the sum game, while on disjoint sum the current player performs a move in exactly one component at each step. A presentation of strategies on coalgebraic games is given via a final coalgebra of a pair of mutually recursive functors, and a suitable notion of simulation. A monoidal closed category of coalgebraic multigames in the vein of a Joyal category of Conway games is then built. The relationship between coalgebraic multigames and games is then formalized via an equivalence of the multigame category and a monoidal closed category of coalgebraic games where tensor is selective sum.

CSL Conference 2013 Conference Paper

Innocent Game Semantics via Intersection Type Assignment Systems

  • Pietro Di Gianantonio
  • Marina Lenisa

The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i. e. the subtyping rules and some structural rules.

MFCS Conference 2012 Conference Paper

Categories of Coalgebraic Games

  • Furio Honsell
  • Marina Lenisa
  • Rekha Redamalla

Abstract We consider a general notion of coalgebraic game, whereby games are viewed as elements of a final coalgebra. This allows for a smooth definition of game operations ( e. g. sum, negation, and linear implication) as final morphisms. The notion of coalgebraic game subsumes different notions of games, e. g. possibly non-wellfounded Conway games and games arising in Game Semantics à la [AJM00]. We define various categories of coalgebraic games and (total) strategies, where the above operations become functorial, and induce a structure of monoidal closed or *-autonomous category. In particular, we define a category of coalgebraic games corresponding to AJM-games and winning strategies, and a generalization to non-wellfounded games of Joyal’s category of Conway games. This latter construction provides a categorical characterization of the equivalence by Berlekamp, Conway, Guy on loopy games.

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.

TCS Journal 2008 Journal Article

A type assignment system for game semantics

  • Pietro Di Gianantonio
  • Furio Honsell
  • Marina Lenisa

We present a type assignment system that provides a finitary interpretation of lambda terms in a game semantics model. Traditionally, type assignment systems describe the semantic interpretation of terms in domain-theoretic models. Quite surprisingly, the type assignment system presented in this paper is very similar to the traditional ones, the main difference being the omission of the subtyping rules.

TCS Journal 2004 Journal Article

Category theory for operational semantics

  • Marina Lenisa
  • John Power
  • Hiroshi Watanabe

We use the concept of a distributive law of a monad over a copointed endofunctor to define and develop a reformulation and mild generalisation of Turi and Plotkin's notion of an abstract operational rule. We make our abstract definition and give a precise analysis of the relationship between it and Turi and Plotkin's definition. Following Turi and Plotkin, our definition, suitably restricted, agrees with the notion of a set of GSOS-rules, allowing one to construct both an operational model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step operational semantics from small-step operational semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of operational semantics with congruences.

LPAR Conference 2003 Conference Paper

Strict Geometry of Interaction Graph Models

  • Furio Honsell
  • Marina Lenisa
  • Rekha Redamalla

We study a class of “wave-style” Geometry of Interaction (GoI) λ -models based on the category Rel of sets and relations. Wave GoI models arise when Abramsky’s GoI axiomatization, which generalizes Girard’s original GoI, is applied to a traced monoidal category with the categorical product as tensor, using “countable power” as the traced strong monoidal functor! . Abramsky hinted that the category Rel is the basic setting for traditional denotational “static semantics”. However, Rel, together with the cartesian product, apparently escapes Abramsky’s original GoI construction. Here we show that Rel can be axiomatized as a strict GoI situation, i. e. a strict variant of Abramsky’s GoI situation, which gives rise to a rich class of strict graph models. These are models of restrictedλ -calculi in the sense of [HL99], such as Church’s λ -I-calculus and the λβ KN -calculus.

CSL Conference 2001 Conference Paper

Fully Complete Minimal PER Models for the Simply Typed lambda-Calculus

  • Samson Abramsky
  • Marina Lenisa

Abstract We show how to build a fully complete model for the maximal theory of the simply typed λ-calculus with k ground constants, λ k. This is obtained by linear realizability over an affine combinatory algebra of partial involutions from natural numbers into natural numbers. For simplicitly, we give the details of the construction of a fully complete model for λ k extended with ground permutations. The fully complete minimal model for λ k can be obtained by carrying out the previous construction over a suitable subalgebra of partial involutions. The full completeness result is then put to use in order to prove some simple results on the maximal theory.

CSL Conference 2000 Conference Paper

A Fully Complete PER Model for ML Polymorphic Types

  • Samson Abramsky
  • Marina Lenisa

Abstract We present a linear realizability technique for building Partial Equivalence Relations (PER) categories over Linear Combinatory Algebras. These PER categories turn out to be linear categories and to form an adjoint model with their co-Kleisli categories. We show that a special linear combinatory algebra of partial involutions, arising from Geometry of Interaction constructions, gives rise to a fully and faithfully complete model for ML polymorphic types of system F.

MFCS Conference 2000 Conference Paper

Axiomatizing Fully Complete Models for ML Polymorphic Types

  • Samson Abramsky
  • Marina Lenisa

Abstract We present axioms on models of system F, which are sufficient to show full completeness for ML-polymorphic types. These axioms are given for hyperdoctrine models, which arise as adjoint models, i. e. co-Kleisli categories of linear categories. Our axiomatization consists of two crucial steps. First, we axiomatize the fact that every relevant morphism in the model generates, under decomposition, a possibly infinite typed Böhm tree. Then, we introduce an axiom which rules out infinite trees from the model. Finally, we discuss the necessity of the axioms.

TCS Journal 1999 Journal Article

Semantical analysis of perpetual strategies in λ-calculus

  • Furio Honsell
  • Marina Lenisa

Perpetual strategies in λ-calculus are analyzed from a semantical perspective. This is achieved using suitable denotational models, computationally adequate with respect to the observational (operational) equivalence, ≈ p, induced by perpetual strategies. A necessary and sufficient condition is given for an ω-algebraic lattice, isomorphic to the space of its strict continuous self-maps, to be computationally adequate w. r. t. ≈ p. While many such models exist, it is shown, however, that none is fully abstract w. r. t. ≈ p. The computationally adequate lattice model Dp is studied in detail. It is used to give a semantical proof of the Conservation Theorem for the λ-calculus, and to provide coinductive and mixed inductive-coinductive characterizations of ≈ p. The coinductive characterization allows to show that the term model of ≈ p is a denotational model; this yields a new characterization of perpetual redexes in λ-calculus.

MFCS Conference 1994 Conference Paper

Processes and Hyperuniverses

  • Michael Forti
  • Furio Honsell
  • Marina Lenisa

Abstract We show how to define domains of processes, which arise in the denotational semantics of concurrent languages, using hypersets, i. e. non-wellfounded sets. In particular we discuss how to solve recursive equations involving set-theoretic operators within hyperuniverses with atoms. Hyperuniverses are transitive sets which carry a uniform topological structure and include as a clopen subset their exponential space (i. e. the set of their closed subsets) with the exponential uniformity. This approach allows to solve many recursive domain equations of processes which cannot be even expressed in standard Zermelo-Fraenkel Set Theory, e. g. when the functors involved have negative occurrences of the argument. Such equations arise in the semantics of concurrrent programs in connection with function spaces and higher order assignment. Finally, we briefly compare our results to those which make use of complete metric spaces, due to de Bakker, America and Rutten.

MFCS Conference 1993 Invited Paper

Some Results on the Full Abstraction Problem for Restricted Lambda Calculi

  • Furio Honsell
  • Marina Lenisa

Abstract Issues in the mathematical semantics of two restrictions of the λ-calculus, i. e. λ I -calculus and λ v -calculus, are discussed. A fully abstract model for the natural evaluation of the former is defined using complete partial orders and strict Scott-continuous functions. A correct, albeit non- fully abstract, model for the SECD evaluation of the latter is denned using Girard's coherence spaces and stable functions. These results are used to illustrate the interest of the analysis of the fine structure of mathematical models of programming languages.

v2026.09.13