Author name cluster

Marcello M. Bonsangue

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.

6 papers

2 author rows

I&C Journal 2003 Journal Article

Infinite intersection types

Marcello M. Bonsangue
Joost N. Kok

A type theory with infinitary intersection and union types for an extension of the λ-calculus is introduced. Types are viewed as upper closed subsets of a Scott domain and intersection and union type constructors are interpreted as the set-theoretic intersection and union, respectively, even when they are not finite. The assignment of types to λ-terms extends naturally the basic type assignment system. We prove soundness and completeness using a generalization of Abramsky’s finitary logic of domains. Finally, we apply the framework to applicative transition systems, obtaining a sound a complete infinitary intersection type assignment system for the lazy λ-calculus.

Details DOI

MFCS Conference 2000 Conference Paper

A Compositional Model for Confluent Dynamic Data-Flow Networks

Frank S. de Boer
Marcello M. Bonsangue

Abstract We introduce a state-based language for programming dynamically changing networks which consist of processes that communicate asynchronously. For this language we introduce an operational semantics and a notion of observable which includes both partial correctness and absence of deadlock. Our main result is a compositional characterization of this notion of observable for a confluent sub-language.

Details

I&C Journal 1999 Journal Article

Toward an Infinitary Logic of Domains: Abramsky Logic for Transition Systems

Marcello M. Bonsangue
Joost N. Kok

We give a new characterization of sober spaces in terms of their completely distributive lattice of saturated sets. This characterization is used to extend Abramsky's results about a domain logic for transition systems. The Lindenbaum algebra generated by the Abramsky finitary logic is a distributive lattice dual to an SFP-domain obtained as a solution of a recursive domain equation. We prove that the Lindenbaum algebra generated by the infinitary logic is a completely distributive lattice dual to the same SFP-domain. As a consequence soundness and completeness of the infinitary logic is obtained for a class of transition systems that is computational interesting.

Details DOI

MFCS Conference 1997 Conference Paper

Specifying Computations Using Hyper Transition Systems

Marcello M. Bonsangue
Joost N. Kok

Abstract We study hyper transition systems as a formalism to give semantics to specification languages which support both unbounded angelic and unbounded demonic non-determinism as well as recursion. Hyper transition are a generalization of transition systems and are suited for the specification of computations by means of properties that atomic steps in a computation have to satisfy. As an application we use a hyper transition system to give an operational semantics to the language of Back's refinement calculus. This operational semantics abstracts from the internal configurations and we prove it to be equivalent to the standard weakest precondition semantics. Finally, we propose a refinement relation that preserves the atomic step of a computation and generalizes the simulation relation on ordinary transition systems. This can be used to augment specification languages with a form of concurrency.

Details

TCS Journal 1995 Journal Article

Duality beyond sober spaces: Topological spaces and observation frames

Marcello M. Bonsangue
Bart Jacobs
Joost N. Kok

We introduce observation frames as an extension of ordinary frames. The aim is to give an abstract representation of a mapping from observable predicates to all predicates of a specific system. A full subcategory of the category of observation frames is shown to be dual to the category of T 0 topological spaces. The notions we use generalize those in the adjunction between frames and topological spaces in the sense that we generalize finite meets to infinite ones. We also give a predicate logic of observation frames with both infinite conjunctions and disjunctions, just like there is a geometric logic for (ordinary) frames with infinite disjunctions but only finite conjunctions. This theory is then applied to two situations: firstly to upper power spaces, and secondly we restrict the adjunction between the categories of topological spaces and of observation frames in order to obtain dualities for various subcategories of T 0 spaces. These involve nonsober spaces.

Details DOI

MFCS Conference 1993 Conference Paper

Isomorphisms between Predicates and State Transformers

Marcello M. Bonsangue
Joost N. Kok

Abstract We study the relation between state transformers based on directed complete partial orders and predicate transformers. Concepts like ‘predicate’, ‘liveness’, ‘safety’ and ‘predicate transformers’ are formulated in a topological setting. We treat state transformers based on the Hoare, Smyth and Plotkin power domains and consider continuous, monotonic and unrestricted functions. We relate the transformers by isomorphisms thereby extending and completing earlier results and giving a complete picture of all the relationships.

Details