Arrow Research search

Author name cluster

Mario Coppo

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.

7 papers
2 author rows

Possible papers

7

TCS Journal 2012 Journal Article

Simulation techniques for the calculus of wrapped compartments

  • Mario Coppo
  • Ferruccio Damiani
  • Maurizio Drocco
  • Elena Grassi
  • Eva Sciacca
  • Salvatore Spinella
  • Angelo Troina

The modelling and analysis of biological systems has deep roots in Mathematics, specifically in the field of Ordinary Differential Equations (ODEs). Alternative approaches based on formal calculi, often derived from process algebras or term rewriting systems, provide a quite complementary way to analyse the behaviour of biological systems. These calculi allow to cope in a natural way with notions like compartments and membranes, which are not easy (sometimes impossible) to handle with purely numerical approaches, and are often based on stochastic simulation methods. Recently, it has also become evident that stochastic effects in regulatory networks play a crucial role in the analysis of such systems. Actually, in many situations it is necessary to use stochastic models. For example when the system to be described is based on the interaction of few molecules, when we are at the presence of a chemical instability, or when we want to simulate the functioning of a pool of entities whose compartmentalised structure evolves dynamically. In contrast, stable metabolic networks, involving a large number of reagents, for which the computational cost of a stochastic simulation becomes an insurmountable obstacle, are efficiently modelled with ODEs. In this paper we define a hybrid simulation method, combining the stochastic approach with ODEs, for systems described in the Calculus of Wrapped Compartments (CWC), a calculus on which we can express the compartmentalisation of a biological system whose evolution is defined by a set of rewrite rules.

TCS Journal 2009 Journal Article

Amalgamating sessions and methods in object-oriented languages with generics

  • Sara Capecchi
  • Mario Coppo
  • Mariangiola Dezani-Ciancaglini
  • Sophia Drossopoulou
  • Elena Giachino

We suggest an amalgamation of communication-based programming (centered on sessions) and object-oriented programming, whereby sessions between concurrent threads are amalgamated with methods. In our proposal, threads consist of the execution of session bodies on objects and communicate with each other by asynchronously sending/receiving objects on channels. The response to a session request is based on the name of the request and the class of the object receiving the request. The decision of how to continue a session is based on the class of the object sent/received. Sessions can be delegated to other sessions, although sessions themselves are not first class objects. We demonstrate our ideas through a core language with generic types, SAM g, and an example. We then formalize a small calculus, F SAM g, and prove subject reduction and progress. The latter property is notoriously difficult to achieve in concurrent calculi.

TCS Journal 2002 Journal Article

Strictness, totality, and non-standard-type inference

  • Mario Coppo
  • Ferruccio Damiani
  • Paola Giannini

In this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. We also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. A main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. This leads to a rather direct presentation which involves relatively little mathematical overhead.

TCS Journal 1993 Journal Article

Type inference, abstract interpretation and strictness analysis

  • Mario Coppo
  • Alberto Ferrari

Filter domains (Coppo et al. ,1984) can be seen as abstract domains for the interpretation of (functional) type-free programming languages. What is remarkable is the fact that in filter domains the interpretation of a term is given by the set of its types in the intersection type discipline with inclusion, thus reducing the computation of an abstract interpretation to typechecking. As a main example, an abstract filter domain for strictness analysis of type-free functional languages is presented. The inclusion relation between types representing strictness properties has a complete recursive axiomatization. Type inference rules cannot be complete (strictness being a Π0 1 property), but a complete extension of the type inference system is presented.

I&C Journal 1991 Journal Article

Type inference with recursive types: Syntax and semantics

  • Felice Cardone
  • Mario Coppo

In this paper we study type inference systems for λ-calculus with a recursion operator over types. The main syntactical properties, notably the existence of principal type schemes, are proved to hold when recursive types are viewed as finite notations for infinite (regular) type expressions representing their infinite unfoldings. Exploiting the approximation structure of a model for the untyped language of terms, types are interpreted as limits of sequences of their approximations. We show that the interpretation is essentially unique and that two types have equal interpretation if and only if their infinite unfoldings are identical. Finally, a completeness theorem is proved to hold w. r. t. the specific model we consider for a natural (infinitary) extension of the type inference system.

TCS Journal 1984 Journal Article

Completeness of type assignment in continuous lambda models

  • Mario Coppo

The completeness of Curry's rules for assigning type schemes to terms of the pure lambda-calculus has been proved by Hindley (1983) and Barendregt et al. (1983) using models of syntactic nature. A first result of this paper is a completeness proof with respect to the model P ω (as asked by Scott (1976)). Moreover, an extension of Curry's system in which type schemes can be assigned to the fixed point combinator is introduced, together with a notion of type semantics for which it is proved sound and complete (answering a question of Scott (1980)). Also in this case, completeness is proved with respect to the model P ω. All results also hold for the alternative notions of type semantics proposed by Hindley (1983) and Scott (1976, 1980).

MFCS Conference 1980 Conference Paper

An Extended Polymorphic Type System for Applicative Languages

  • Mario Coppo

Abstract This paper deals with the problem of finding a type system for programming languages, which allows the greatest generality in the definition of polymorphic procedures. The type system introduced in this paper can be seen as an extension of the one proposed in /MLN/ (which is implemented in the language ML). The rules for type assignement are given and their semantic correctness is proved. Moreover, some results about the semantic characterization of typed terms are proved.

v2026.09.13