Browsing by Author "Vasconcelos, Vasco T."
Now showing 1 - 10 of 18
Results Per Page
Sort Options
- Bisimulations in SSCCPublication . Filipe, Luís Cruz; Lanese, Ivan; Martins, Francisco; Ravara, António; Vasconcelos, Vasco T.This report studies different definitions of bisimulation within the Stream-Based Service-Centered Calculus (SSCC) and shows that both strong and weak ground bisimulation are non-input congruences
- Compiling the $\pi$-calculus into a Multithreaded Typed Assembly LanguagePublication . Cogumbreiro, Tiago; Martins, Francisco; Vasconcelos, Vasco T.Current trends in hardware made available multi-core CPU systems to ordinary users, challenging researchers to devise new techniques to bring software into the multi-core world. However, shaping software for multi-cores is more envolving than simply balancing workload among cores. In a near future (in less than a decade) Intel prepares to manufacture and ship 80-core processors; programmers must perform a paradigm shift from sequential to concurrent programming and produce software adapted for multi-core platforms. In the last decade, proposals have been made to compile formal concurrent and functional languages, notably the $\pi$-calculus, typed concurrent objects, and the $\lambda$-calculus, into assembly languages. The last work goes a step further and presents a series of type-preserving compilation steps leading from System F to a typed assembly language. Nevertheless, all theses works are targeted at sequential architectures. This paper proposes a type-preserving translation from the $\pi$-calculus into MIL, a multithreaded typed assembly language for multi-core/multi-processor architectures. We start from a simple asynchronous typed version of the $\pi$-calculus and translate it into MIL code that is then linked to a run-time library (written in MIL) that provides support for implementation of the $\pi$-calculus primitives (e.g., queuing messages and processes). In short, we implement a message-passing paradigm in a shared memory architecture
- Congu, Checking Java Classes Against Property-Driven Algebraic SpecificationsPublication . Abreu, João; Caldeira, Alexandre; Lopes, Antónia; Nunes, Isabel; Reis, Luís S.; Vasconcelos, Vasco T.Congu is a tool that supports the checking of Java classes against property-driven algebraic specifications. This document presents the specification, languages, the tool usage, and its implementation, version 1.32. Chapter 1 describes the two specification languages: the language of abstract data types specifications, and that for defining refinement mappings between these specifications and Java classes. Chapter 2 explains how to install and use Congu tool. And finally, Chapter 3 presents the implementation details of the tool
- Controlling Security Policies in a Distributed EnvironmentPublication . Martins, Francisco; Vasconcelos, Vasco T.This paper presents a type system to control the migration of code between nodes in a concurrent distributed framework, using Dpi. We express resource policies with types and enforce them via a type system. Sites are organised hierarchically in subnetworks that share the same security policies, statically specified by a network administrator. The type system guarantees that, at runtime, there are no security policies violations
- Core-TyCO, The Language Definition, Version 0.1Publication . Vasconcelos, Vasco T.; Bastos, RuiThis is the second report on TyCO, a (still) experimental strongly and implicitly typed concurrent object oriented programming language based on a predicative polymorphic calculus of objects, featuring asynchronous messages, objects, and process declarations, together with a predicative polymorphic type system
- Core-TyCO: Appendix to the Language Definition, yielding Version 0.2Publication . Vasconcelos, Vasco T.This is the third report on TyCO, a (still) experimental strongly and implicitly typed concurrent object based programming language based on a predicative polymorphic calculus of objects, featuring asynchronous messages, objects, and procedures, together with a predicative polymorphic typing assignment system, assigning monomorphic types to variables and polymorphic types to procedures
- Disciplining Orchestration and Conversation in Service-Oriented ComputingPublication . Lanese, Ivan; Vasconcelos, Vasco T.; Martins, Francisco; Ravara, AntónioWe give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when invoked (conversation). The calculus includes primitives for defining and for invoking services, for isolating conversations between requesters and providers of services, and primitives for orchestrating services, that is, to make use of existent services as building blocks to accomplish complex tasks. The calculus is equipped with a reduction and a labeled transition semantics; an equivalence result relates the two. To give an hint on how the structuring mechanisms of the language can be exploited for static analysis we present a simple type system guaranteeing the compatibility between the protocols for service definition and for service invocation, and ensuring the sequentiality of each protocol
- Language Primitives and Type Discipline for Structured Communication-Based Programming, Subject Reduction and Type Safety TheoremsPublication . Vasconcelos, Vasco T.; Yoshida, NobukoSession primitives and types provide a flexible programming style for structural interaction, and are used to statically check the safe and consistent composition of protocols in communication-centric distributed software. Unfortunately authors working on session types have recently realised that some of the previously published systems fail to satisfy the basic theorems of Subject Reduction and Type Safety. This report discusses the issues involved in higher-order session communication, presents a formulation of the recursive types as well as proofs of the Subject Reduction and Type Safety Theorems of the original session typing system by Honda-Vasconcelos-Kubo in ESOP'98. It also proposes a new session typing system which allows a more liberal higher-order session communication based on an idea of Gay and Hole.
- A Lexically Scoped Distributed $\pi$-CalculusPublication . Ravara, António; Matos, Ana; Vasconcelos, Vasco T.; Lopes, LuísWe define the syntax, the operational semantics, and a type system for lsd-pi, an asynchronous and distributed $\pi$-calculus with local communication and process migration. The calculus follows a simple model of distribution for mobile calculi, with a lexical scoping mechanism that provides both for remote communication and for process migration, making explicit migration primitives superfluous
- Proceedings of the First Workshop on Programming Language Approaches to Concurrency and Communication-cEntric SoftwarePublication . Vasconcelos, Vasco T.; Yoshida, NobukoThis documents contains the proceedings of PLACES'08, the 1st Workshop on Programming Language Approaches to Concurrency and Communication- cEntric Software, held in Oslo, Norway, on June 7, 2008, co-located with the DisCoTec federated conferences. PLACES aims to offer a forum where researchers from different Þelds ex- change new ideas on one of the central challenges in programming in near future, the development of programming methodologies and infrastructures where con- currency and distribution are a norm rather than a marginal concern. The Program Committee, after a careful and thorough reviewing process, se- lected for inclusion in the programme 10 papers out of 14 submissions. Each submission was evaluated by at least two referees, and the accepted papers were selected during one week electronic discussions. The volume opens with the abstracts for the invited contributions by Jan Vitek (Purdue University) and and Alan Mycroft (University of Cambridge), and con- tinues with the ten technical papers. Places'08 was made possible by the contribution and dedication of many peo- ple. First of all, we would like to thank all the authors who submitted papers for consideration. Secondly we would like to thank our invited and tutorial speakers. We would also like to thank the members of the Program Committee for their care- ful reviews, and the balanced discussions during the selection process. Dimitris Mostrous helped to set up a web page for the PC discussion. Finally, we acknowl- edge the Discotec general chairs, Frank Eliassen and Einar Broch Johnsen, and the Workshop chair Amy L. Murphy