Seminars

  • Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication.

    Vasco T. Vasconcelos

    Abstract: 

    Session primitives and types provide a flexible programming style for structural interaction, and are used to statically check a safe and consistent composition of protocols in communication-centric distributed software. They have been studied for the pi-calculus, Ambients, CORBA interfaces, multi-threaded functional languages, Web Description Languages, and distributed and multi-threaded Java. In the presence of higher-order session communication, session instantiation dynamically changes structures of sessions during execution, so that it becomes non-trivial to preserve typability. Unfortunately authors working on session types have recently realised that some of the previous systems fail to satisfy Subject Reduction. Interestingly, the subtlety of type preservation is related to a treatment of communication channels in the rewriting rules of the pi-calculus. After discussing the issues involved in higher-order session communication, we also propose a new session typing system which allows a more liberal higher-order session communication based on an idea of Gay and Hole. [Joint work with Nobuko Yoshida]

    Where: 
    6.3.5
    When: 
    Wednesday, May 31 2006
    Time: 
    11:00
  • Checking the Conformance of Java Classes Against Algebraic Specifications.

    Isabel Nunes

    Abstract: 

    We present and evaluate an approach for the run-time conformancechecking of Java classes against property-driven algebraic specifications.Ourproposal consists in determining, at run-time, whether the classes subject toanalysisbehave as required by the specification. The key idea is to reduce theconformancechecking problem to the runtime monitoring of contract-annotated classes,a process supported today by several runtime assertion-checking tools.Our approach comprises a rather conventional specification language, a simplelanguage to map specifications into Java types, and a method to automaticallygenerate monitorable classes from specifications, allowing for a simple, buteffective,runtime monitoring of both the specified classes and their clients. [Join work with Antónia Lopes, Vasco Vasconcelos, João Abreu, and Luís Reis]

    Where: 
    6.3.5
    When: 
    Wednesday, May 24 2006
    Time: 
    11:00
  • A Multithreaded Typed Assembly Language.

    Francisco Martins

    Abstract: 

    We present an assembly language targeted at shared memory multiprocessors, where CPU cores synchronize via locks, acquired with a traditional test and set lock instruction. We show programming examples taken from the literature on Operating Systems, and discuss a typing system that enforces a strict protocol on lock usage and that prevents race conditions. [Joint work with Vasco Vasconcelos].

    Where: 
    6.3.5
    When: 
    Wednesday, May 17 2006
    Time: 
    11:00
  • Spatial-Behavioral Types for Distributed Services.

    Luis Caires

    Abstract: 

    We discuss a type system, motivated by dynamic spatial logic, that may beused to discipline distributed interactions in service-based systems. Inour system types denote spatial-behavioral properties definable in spatiallogic, enabling us to formulate semantical soundness arguments (cf.logical relations) for the typing and subtyping relations.

    Where: 
    6.3.5
    When: 
    Wednesday, May 10 2006
    Time: 
    11:00
  • Role-Based Declarative Synchronization for Reconfigurable Systems.

    Pawel Wojciechowski

    Abstract: 

    In this talk we address the problem of encoding complexconcurrency control in reconfigurable systems. Such systems can be often reconfigured, either statically, or dynamically, in order to adapt to new requirements and a changing environment.We therefore take a declarative approach and introduce a set of high-level programming abstractions which allow the programmer to easily express complex synchronization constraints in multithreaded programs. The constructs are based on our model of role-based synchronization (RBS) which assumes attaching roles to concurrent threads and expressing a synchronization policy between the roles. The model will be illustrated by describing an experimental implementation of our language as a design pattern library in OCaml. Finally, we also say about a small application of a web access server that we have implemented using the RBS design pattern.

    Where: 
    6.3.5
    When: 
    Friday, April 15 2005
    Time: 
    11:00
  • Processes with liveness requirements.

    Helia Guerra

    Abstract: 

    In the deterministic quiescent model, introduced by Costa andSernadas in the mid of 90s, new insights on quiescence were givenconcerning the Jonsson's characterisation through the introduction oftwo kinds of prefixing: active and passive, providing a tool tospecify transactional behaviour for systems. This model captures new(local and finite) liveness properties of concurrent and distributedsystems, which are typically specified in temporal logic but notcaptured by process algebras, because their semantics imposes prefixclosed sets for traces. Inspired by this work, we had also beenenriched this model with new operators in order to capture moreliveness properties but directly from process algebra itself. Our workwas going beyond the finite quiescence, through an extension of thequiescent model in order to capture infinite liveness requirementsand, thus, introducing infinite transactional behaviours.Capitalising the well-known Hennessy's semantic approach of semantictrinity, we provide three equivalent semantic domains (denotational,axiomatic and operational) for both extensions. [Joint work withJ. Felix Costa]

    Where: 
    6.3.5
    When: 
    Wednesday, January 19 2005
    Time: 
    11:00
  • MIkado Koncurrent Objects (MIKO).

    Liliana Salvador

    Abstract: 

    We present an instance of the Mikado membrane model (vide A parametric model of migration and mobility, A generic membrane model) using the TyCO core calculus. The model is based on the concept of domain, a named site with a membrane and a content, where the membrane controls the migration of code in a network of distributed processes.

    Where: 
    6.3.5
    When: 
    Wednesday, December 15 2004
    Time: 
    11:00
  • A language for datatype specification.

    Isabel Nunes

    Abstract: 

    Discutimos uma linguagem de especificação de tipos de dados abstratos para geração de contratos JML/Java.

    Where: 
    6.3.5
    When: 
    Wednesday, November 24 2004
    Time: 
    11:00
  • History-based access control for distributed processes.

    Francisco Martins

    Abstract: 

    We present a type system to control the migration of code between nodes in a distributed environment. No! It's not more of the same... now types describe paths travelled by migrating code, enabling an history sensitive access discipline to resources. Don't miss it! ;-)

    Where: 
    6.3.5
    When: 
    Wednesday, November 10 2004
    Time: 
    11:00
  • Subtyping first class polymorphic components.

    João Costa Seco

    Abstract: 

    We present a statically typed, class-based object oriented language where classes are first class polymorphic values. A main contribution of this work is the design of a type system that combines first class polymorphic values with structural equirecursive types and admits a subtyping algorithm which is arguably much simpler than existing alternatives. The type inference system is decidable and possesses the minimal type property.

    Where: 
    6.3.5
    When: 
    Wednesday, November 3 2004
    Time: 
    11:00

Pages

Subscribe to Seminars