Encontros de Quarta-Feira

Pretendem os Encontros de Quarta-Feira ser um espaço de discussão de temas de interesse comum: concorrência, especificação e verificação, objectos.
October 24, 2007. Ricardo Martinho. Towards a flexibility framework for software processes
Software process models are dynamic entities that must evolve in order to cope with changes occurred in: the enacting process (due to changing requirements or unforeseen circumstances); the software development organization; the market; and in the methodologies used to produce software. Therefore, flexibility concepts should also be part of a process modeling meta-model, in order for process modelers to be able to express the "right" flexibility into process models, i.e., to express which, where and how flexible are the elements that compose a process model. In this workshop I'll talk about how SPEM-based software process models can support and express flexibility concepts, and also about some early developments regarding an implementation of those concepts.
September 26, 2007. Hugo Miranda. Distribuição de dados utilizando algoritmos epidémicos em redes ad hoc sem fios (Gossip-based data distribution in mobile ad hoc networks)
Redes ad hoc sem fios são redes de dados construidas sem o apoio de uma infra-estrutura de suporte e compostas exclusivamente por dispositivos móveis. Assume-se que os dispositivos móveis têm recursos limitados (energia, memória e poder computacional) e podem mover-se livremente, entrando e saindo do raio de transmissão dos restantes com frequência. Devido à ausência de uma infra-estrutura de suporte, os serviços (e.g. encaminhamento, armazenamento de dados) têm que ser prestados pelos próprios dispositivos, muitas vezes de forma cooperativa para aumentar a resiliência a falhas. A apresentação descreve uma concretização de um serviço de replicação de dados em redes ad hoc sem fios. Serão abordados os diversos algoritmos necessários à disseminação e recuperação de dados e apresentada uma aplicação para este serviço.
July 11, 2007. Carla Ferreira. Modeling compensations in mobile processes.
We add to the asynchronous pi-calculus primitives to deal with compensation, namely to define, store, and activated the execution of, compensations. Some simple examples illustrate the expressiveness of the language. We extend the usual operational semantics (both the reduction relation and the label transition system) with rules treating the new constructs, and show that bisimulation is a congruence. [Joint work with António Ravara]
February 28, 2007. Dimitris Mostrous. Session Types for Object-Oriented Languages.
This talk presents recent work on the integration of session types to a small concurrent Java-like calculus. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other party. Session types characterise such behaviour in terms of the types of values communicated and the shape of protocols, and have been developed for the Pi and Ambient calculi, CORBA interfaces, Haskell, multithreaded functional languages, the C language, and web description languages. We present the incorporation of session types into object-oriented languages through the language Moose, a multi-threaded language with session types, thread spawning, iterative and higher-order sessions. We describe the design of Moose, its syntax, operational semantics and type system, and show a number of important properties of the language: type inference, type soundness, progress, and communication error freedom. [Joint work with Mariangiola Dezani (Torino), Nobuko Yoshida (Imperial), and Sophia Drossopoulou (Imperial)]
February 21, 2007. António Ravara. Cryptographic primitives in a calculus with polyadic synchronisation.
We define cryptographic primitives for the pi-calculus extended with polyadic synchronisation (epi), and show that this primitives are derivable constructs, ie, epi with cryptographic primitives may be fully abstractly encoded in the regular epi. The proposed encoding is sound and complete wrt barbed congruence, which, as we also show, coincides with early bisimilarity. [Joint work with Joana Martinho and Luca Aceto]
February 7, 2007. Carla Ferreira. Comparing two approaches to compensable flow composition.
In this talk it will be discussed two process algebras (cCSP and Sagas) for modelling web services composition. Although both algebras are focused on the formalisation of compensatable processes, each notation supports a different compensation policy.
January 24, 2007. Francisco Martins. Shared Read Access and Linear Ownership in a Typed Assembly Language.
We present an extended type system for a typed assembly language that allows for shared reading access to memory and that controls the linear ownership of memory tuples.
January 11, 2007. Vasco T. Vasconcelos. A Stream-based Core Calculus for Services.
We present a calculus that aims at describing, in a unique framework, both individual services (and in particular the conversation between clients and servers after service invocation), and the coordination necessary to compose different services (the orchestration of concurrent and distributed services). Emphasis on the connection with Orc and with Modelling in Service-Oriented Architectures. [Joint work with Ivan Lanese, António Ravara, Francisco Martins.]
July 12, 2006. André Santos. Framework Specialization Aspects.
In this talk I will explain the advantages of using aspect-oriented programming (AOP) in the context of object-oriented frameworks. Variability requirements are taken into account in framework design by defining hot spots. Hot spots rely on (compositions of) design patterns. A hot spot extension implements a certain variable part in a framework specialization. I will show that this necessarily leads to code scattering/tangling in framework specializations, considering separation of concerns according to hot spot extensions. Having a framework, my approach consists in developing "specialization aspects" - abstract aspects that support a modularized interface for hot spot extension, and in turn, a modularized implementation of the hot spot extensions. Moreover, the approach evidences other benefits concerning increased reuse within specializations and lower coupling between framework and specializations. I've been carrying out a case study using the JHotDraw framework and I'll show some concrete results on applying the approach.
June 28, 2006. Maxime Gamboni. Deciding Deterministic Responsiveness and Closeness in pi-calculus.
I'll describe a type system for data structure encodings in pi, that checks process parts storing encoded data so that a decoding request is replied once, deterministically, uniformly and without side effects.
June 21, 2006. Hugo Torres Vieira. Extensionality of Spatial Observations in Distributed Systems.
We discuss the tensions between intensionality and extensionality of spatial observations in distributed systems, showing that there are models where observational equivalences may be characterized by spatial logics, including the composition and void operators. Our results support the claim that spatial observations do not need to be always considered intensional, even if expressive enough to talk about the stucture of systems. [Joint work with Luís Caires]
June 7, 2006. Antónia Lopes. A Formal Approach to Service Component Architectures.
In this talk I will report on an algebraic framework being developed within the SENSORIA project for supporting service-oriented modelling at high levels of abstraction, i.e. independently of the hosting middleware and hardware platforms, and the languages in which services are programmed. More specifically, I will give an account of the notion of module that supports the composition model of SENSORIA, which includes interfaces for required (imported) and provided (exported) services, as well as a number of components (body) whose orchestrations ensure how given behavioural properties of the provided services are guaranteed assuming that the requested services satisfy required properties. [Joint work with José Fiadeiro and Laura Bocchi]
May 31, 2006. Vasco T. Vasconcelos. Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication.
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]
May 24, 2006. Isabel Nunes. Checking the Conformance of Java Classes Against Algebraic Specifications.
We present and evaluate an approach for the run-time conformance checking of Java classes against property-driven algebraic specifications. Our proposal consists in determining, at run-time, whether the classes subject to analysis behave as required by the specification. The key idea is to reduce the conformance checking 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 simple language to map specifications into Java types, and a method to automatically generate monitorable classes from specifications, allowing for a simple, but effective, 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]
May 17, 2006. Francisco Martins. A Multithreaded Typed Assembly Language.
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].
May 10, 2006. Luis Caires. Spatial-Behavioral Types for Distributed Services.
We discuss a type system, motivated by dynamic spatial logic, that may be used to discipline distributed interactions in service-based systems. In our system types denote spatial-behavioral properties definable in spatial logic, enabling us to formulate semantical soundness arguments (cf. logical relations) for the typing and subtyping relations.
April 15, 2005. Pawel Wojciechowski. Role-Based Declarative Synchronization for Reconfigurable Systems.
In this talk we address the problem of encoding complex concurrency 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.
January 19, 2005. Helia Guerra. Processes with liveness requirements.
In the deterministic quiescent model, introduced by Costa and Sernadas in the mid of 90s, new insights on quiescence were given concerning the Jonsson's characterisation through the introduction of two kinds of prefixing: active and passive, providing a tool to specify transactional behaviour for systems. This model captures new (local and finite) liveness properties of concurrent and distributed systems, which are typically specified in temporal logic but not captured by process algebras, because their semantics imposes prefix closed sets for traces. Inspired by this work, we had also been enriched this model with new operators in order to capture more liveness properties but directly from process algebra itself. Our work was going beyond the finite quiescence, through an extension of the quiescent model in order to capture infinite liveness requirements and, thus, introducing infinite transactional behaviours. Capitalising the well-known Hennessy's semantic approach of semantic trinity, we provide three equivalent semantic domains (denotational, axiomatic and operational) for both extensions. [Joint work with J. Felix Costa]
December 15, 2004. Liliana Salvador. MIkado Koncurrent Objects (MIKO).
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.
November 24, 2004. Isabel Nunes. A language for datatype specification.
Discutimos uma linguagem de especificação de tipos de dados abstratos para geração de contratos JML/Java.
November 10, 2004. Francisco Martins. History-based access control for distributed processes.
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! ;-)
November 3, 2004. João Costa Seco. Subtyping first class polymorphic components.
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.
June 30, 2004. Maxime Gamboni. What's TyCO, after all?.
Pi-a-v is an extension of asynchronous Pi-calculus, where transmitted values are names optionally tagged with any numbers of labels. Uniform TyCO can be seen as a sub-calculus of Pi-a-v (where each value is a name with exactly one label), the only difference being that Pi-a-v requires a separate construct for analysing a value while in TyCO input and value analysis are tightly bound. We study the expressive power of these two calculi by means of encodings. We can give an encoding (embedding) of TyCO to Pi-a-v that is good and fully abstract. We propose an encoding from local Pi-a-v to TyCO and show that it is fully abstract.
June 9, 2004. Paulo Carreira. Execution of Data Mappers.
Data mappers are essential operators for implementing data transformations supporting schema mapping and integration scenarios such as legacy data migration, ETL processes for data warehousing, data cleaning activities, and business integration initiatives. Despite their widespread use, no formalization of this important operation has been proposed so far. In this paper we propose the data mapper operator as an extension to the relational algebra. We supply a set of algebraic rewriting rules for optimizing queries that combine standard relational operators with data mappers. Finally, we analyze possible algorithms for their efficient physical execution.
June 2, 2004. Luís Caires. Implementing shared key cryptographic protocols in the Pi-Calculus.
We discuss a simple technique for representing shared key cryptographic protocols in the pi-Calculus. The basic idea underlying the encoding is not new: it already appears in an early discussion of Abadi and Gordon about candidate encodings of the spi calculus into the pi calculus, where some counterexamples to their soundness are also given, and also in recent work by Victor, Baldamus and Parrow, where several obstacles to full-abstraction are discussed. In this talk, we remark that under certain natural assumptions there is indeed a fully-abstract encoding of spi processes into pi processes that allows standard bisimulation-based techniques to be applied on the target calculus.
May 26, 2004. Francisco Martins. Resource access typing in Open Systems.
We discuss the ideas introduced by Riely and Hennessy (techical report) about trust and partial typing in open systems. The authors propose a type system to control resource access in open distributed systems in which some sites may execute malicious code that interacts with code running at good sites. In the second part of the talk we examine the proposal by Gorla and Pugliese concerning dynamic acquisition of privileges to control resource access (paper). They propose a type system that checks privileges statically, and mark those actions not possible to check at compile time to be checked at.
May 5, 2004. Vasco Vasconcelos. Session Types for Functional Multithreading.
We define a multi-threaded functional language whose type system allows complex protocols to be specified by types and verified by static typechecking...
Oh no, session types again! We now have: concurrency, allowing to talk about inter-thread communication; polymorphism, providing for code reuse; and a type checking algorithm, allowing for a compiler to statically check protocols. [Joint work with Simon Gay and António Ravara].
April 28, 2004. Xudong Guan. Encoding Pi-Calculus In Ambients.
This talk is about encodings of pi-calculus in ambient. The result was first given by Zimmer in his EXPRESS'00 paper. I will first present a revised encoding scheme from asynchronous-pi to safe ambient without communications. If there is more time, I will talk about my recent draft idea of a new proof of the encoding. (paper).
April 21, 2004. Luís Caires. Decidibilidade e Indecidibilidade das Lógicas Espaciais para a Concorrência.
March 31, 2004. Carla Ferreira. A process compensation language.
StAC (Structured Activity Compensation) is a business process modelling language and distinctive feature of this language is its support for compensation. A compensation is an action taken to recover from error or cope with a change of plan, especially when rollback of a process is not possible. StAC is similar to a process algebraic language such as Hoare's CSP or Milner's CCS but has additional operators dealing with compensation and with exception handling. This talk presents the StAC language and discusses its operational semantics.
March 17, 2004. António Ravara. Typing polyadic synchronisation.
O cálculo-pi com sincronizacao poliadica foi proposto por Carbone e Maffeis recentemente (paper). A ideia é sincronizar não apenas num nome mas num vector de nomes. Esta variante revelou-se muito expressiva, sendo capaz de internalizar o mecanismo de matching, o que não acontece com o cálculo-pi. Além de fazer uma apresentação do referido artigo vou falar também de trabalho em curso para desenvolver um sistema de tipos para o cálculo.
March 3, 2004. Francisco Martins. Controlling security policies in a distributed environment.
We present a type system that allow us to express and control security policies in a distributed framework. It uses Dpi as the underlying calculus and, on top of it, defines an hierarchical structure of security groups. The security model we propose is based on the notion of security groups and constitute an experiment of the Mikado core model, exploring the role of domain guardians. A security group delimits a region of the network with the same security requirements and may be understood as a firewall that dictates and supervises the sites under its control. The language we choose to write security policies is very simple and is expressed as type system assumptions. In fact, we use a type system as the security mechanism to enforce that networks respect the security policies defined by groups. Beyond the Mikado core model we investigate two further directions: (a) the decoupling of the guardian part of the domain from its computational area and (b) the study of a different hierarchy model to express the dependencies between security groups.
January 21, 2004. Antónia Lopes. Software Fiável via Análise Estática.
Breve panorâmica sobre Análise Estática de Programas e o seu papel na obtensão de software fiável. Serão abordadas técnicas e métodos que permitem predizer o comportamento de um programa em tempo de execução baseado na análise directa do seu código, nomeadamente a Interpretação Abstracta e a análise de Fluxo de Dados. Será ainda abordada a integração de técnicas de Análise Estática com técnicas de Verificação de Modelos. Abstract interpretation and semantics.
December 10, 2003. Isabel Nunes. Three topics on design by contract.
Three topics will be introduced and discussed - hopefully a very fruitful discussion with lots of good ideas emerging.
i) How to prevent the increasing of class coupling that arises in the process of contract construction: see UML'03 and Design by Contract Using Meta-Assertions
ii) Redefinition of methods: we claim that the rules for contract refinement are much too strong. See a draft (not published)
iii) How to prevent invariant violations due to representation exposure (the invariant of a class is violated due to some change that is out of its instances control); more generally, how to deal with representation exposure, aliasing? see draft (not published); see reference stuff on this matter; more; and more.
December 17, 2003. Joana Martinho. Comparação dos sistemas de transição early e late do cálculo pi.
O cálculo pi introduzido por Milner, Parrow e Walker é usado para modelar processos que podem ser dinamicamente reconfigurados. Para este cálculo foram propostos dois sistemas de transição que diferem no tratamento da transição de input; um que corresponde à instanciação antecipada do parâmetro (early) e outro à instanciação tardia do mesmo (late). Uma vez que o sistema de transição utilizado influencia as noções de bissimulação que podem ser introduzidas, surge naturalmente a questão de relacionar estas equivalências. Nesta apresentação consideramos as quatro variantes de bissimulação conhecidas na literatura: open, early, late e ground, expomos a sua hierarquia no caso do sistema de transição late e alguns resultados para o caso do sistema de transições early. Links: A Calculus of Mobile Processes, Part I; Part II
26 Junho 2002.
Antónia Lopes. Primitivas arquitectónicas para a Distribuição e a Mobilidade. Com o objectivo de obter uma abordagem arquitectónica para a Distribuição e Mobilidade, tem-se vindo a investigar a adição desta nova dimensão à abordagem arquitectónica baseada no CommUnity. Neste encontro serão apresentados alguns dos passos já dados nesta direcção. Apresenta-se uma extensão do CommUnity que suporta a descrição dos aspectos dos sistemas relacionados com a distribuição e a mobilidade. Propõe-se uma primitiva arquitectónica que permite representar explicitamente nas arquitecturas dos sistemas mecanismos relacionados com a distribuição e a mobilidade.
22 Maio 2002.
Simon Gay, Department of Computing Science, University of Glasgow. Bounded Polymorphism in Session Types Session types in the pi calculus, introduced by Honda, Takeuchi and Kubo, allow complex patterns of communication to be specified and typechecked: the definition of a protocol can be converted into a type, and static typechecking can verify that a client or server implementation uses the protocol correctly. Later developments by Honda, Vasconcelos and Kubo, and by Gay and Hole, added flexibility to session types by allowing session channels to be transmitted between processes, and by defining a notion of subtyping. In this talk I will describe joint work with my student Malcolm Hole, in which we use our system of session types with subtyping as the basis for a form of bounded polymorphism. This extension allows more protocols to be typechecked.
27 Março 2002.
Antónia Lopes. Panorâmica sobre o programa da disciplina de complexidade, Parte II.
20 Março 2002.
Antónia Lopes. Panorâmica sobre o programa da disciplina de complexidade, Parte I.
24 Abril 2001.
Isabel Nunes. Bridging the gap entre especificações de TDAs e especificações dos interfaces OO que descrevem possíveis implementações. O objectivo é a definição de regras tanto ao nível de construção de especificações de Tipos de Dados Abstractos como ao nível da sua transformação em especificações (assinaturas de métodos e respectivas pré e pós condições) de interfaces ou classes que os implementam. Estas regras, para uma dada linguagem de especificação de TDAs e para um dado par linguagem POO e linguagem de asserçoes, definiriam um processo automático de transformação que, dada uma especificação de um TDA como input, devolveria a especificação de um interface OO descrevendo possíveis implementações do TDA. Esboça-se e põe-se à discussão aqui: i) definição do conjunto de especificações de TDAs passíveis de serem transformadas em especificações de interfaces ou classes (assinaturas de métodos e respectivas pré e pós condições); ii) regras para essa transformação. A linguagem POO Java e uma linguagem de asserções à la iContract são usadas nos exemplos apresentados.
6 Dezembro 2001.
Isabel Nunes. First Level Assertions. Writing assertions for methods in classes such as Stack, Point, Account is something that is being taught in many undergraduate courses that include design by contract. Students can even see "assertions at work" using the tools associated with several assertion languages, e.g, iContract, JML, etc. When we have to write pre- and post-conditions for methods in classes that use those simple classes, and furthermore, in classes that use those upper level classes, the task reveals itself harder and harder. The way we usually write pre and post-conditions, when applied to upper level classes, can bring undesirable effects, like the increasing in class coupling. An extension to the usual assertion languages is proposed that allows to write first-level assertions obviating the problem of increased coupling.

29 Novembro 2001.
António Casimiro. Timely Actions in the Presence of Uncertain Timeliness. Many services to be provided over current large-scale, unpredictable and unreliable infrastructures have timeliness requirements. This creates a difficult-to-solve contradiction with regard to the adequate time model: synchronous, or asynchronous? We propose an architectural construct and programming model, the Timely Computing Base (TCB), which addresses the problem in a generic way. We show that with a TCB it is possible to build dependable and timely applications exhibiting varying degrees of timing fault tolerance, under several synchrony models.
22 Novembro 2001.
João Pedro Neto. Symbolic Computations with Neural Nets Programming languages can be translated efficiently on recurrent (analog, rational weighted) neural nets, using bounded resources. This fact was achieved by creating a neural programming language called NETDEF, such that each program corresponds to a modular neural net that computes it. This framework has also some practical implications in recent efforts to merge symbolic and sub-symbolic computation.
15 Novembro 2001.
António Branco. Cognitive and computational models of anaphora. Very broadly speacking, natural language anaphors --- such as "he", "ourselves", "the students", "John", "then", "too", etc. --- behave semantically like variables do in artificial languages. We introduce the mainstream rationale of cognition-based explanations to the interpretation of anaphora, specially in what concerns the detection of variable binders ('anaphor resolution' in language engineering parlance). We discuss why this rationale, built upon the notions of working memory size, attentional prominence degree and computational economy, is arguably not the correct explicative model for anaphora.
8 Novembro 2001.
Luís Caires. Uma lógica espacial para sistemas concorrentes (trabalho conjunto com Luca Cardelli). Apresenta-se uma lógica que permite exprimir propriedades de privacidade, estrutura e comportamento em sistemas concorrentes. Para além das operações lógicas usuais, a lógica que propomos inclui operações espaciais, correspondendo à composição paralela e à restrição local de nomes, e um quantificador primitivo sobre nomes frescos. As propriedades podem também ser definidas recursivamente, um tema central deste trabalho é a combinação de um noção lógica de frescura com a definição indutiva e coindutiva de propriedades.
25 Outubro 2001.
Vasco Thudichum Vasconcelos. A redução determinista comuta com a congruência farpada forte. Poder-se-ia tratar de um exercício precedido de um asterisco, no último livro sobre o cálculo pi. No caso do cálculo-pi síncrono e para a relação de congruência farpada forte (um passo de redução imitado por um só passo de redução), está em aberto se a redução comuta com a congruência. Isto porque está em aberto se a bisimulação coincide com a congruência farpada. No caso particular da redução determinista podemos provar o resultado. O exercício é interessante pelo conjunto de técnicas utilizadas: indução na profundidade do buraco dum contexto, técnica da bissimulação up-to, construção dum contexto muito especial. [A prova é de D. Sangiorgi.]
18 Outubro 2001.
Francisco Martins. Linear channels detection for TyCO We present an extension to the TyCO type system where we can identify linear channels (a channel that can be used at most for a single input and a single output operation). Moreover, we devise an algorithm to reconstruct channels usage information from process expressions.
11 Outubro 2001.
Claudio Hermida. A categorical outlook on relational modalities We show how the modalities < > and [ ] arise canonically by extension of a predicate logic from functions to relations. We apply the resulting fibrational interpretation of modalities to exhibit an intrinsic relationship between satisfaction of modal formulae in a transition system and simulations.
6 Junho 2001.
Dulce Domingos. Linguagem de políticas de segurança e desenho orientado por objectos. No desenvolvimento de um sistema de informação seguro devem ser considerados os requisitos de segurança desde o seu início. Com este objectivo, pretende-se estender as metodologias de análise e desenho orientados por objectos de modo a integrarem as metodologias da engenharia de segurança. Um dos aspectos importantes é a definição de uma linguagem de políticas de segurança com características que permitam (1) a sua utilização na formalização de vários tipos de políticas de segurança, (2) a sua interligação com a fase de desenho, respeitando o paradigma dos objectos e (3) a análise da coerência da política de segurança definida.
23 Maio 2001.
Hugo Miranda. Plataforma de suporte ao desenvolvimento e composição de malhas de protocolos. Os sistemas de suporte à comunicação recentes oferecem um ambiente onde cada programador compõe o conjunto de módulos que satisfaz as propriedades necessárias à aplicação que se encontra a desenvolver. Cada sistema pode ser caracterizado pelas opções que toma para um conjunto de factores como o momento de ligação dos módulos ou as ferramentas disponíveis para a troca de mensagens. A apresentação descreve alguns dos sistemas recentes, analisando o impacto que as opções apresentam no produto final. Mostra que os modelos de composição utilizados são insuficientes para uma classe de aplicações com requisitos emergentes nas redes de computadores e descreve o Appia: um novo sistema de suporte à composição.

16 Maio 2001.
Vasco Thudichum Vasconcelos. TyCO Gently. TyCO stands for ``TYped Concurrent Objects''. Not that the language includes any form of primitive objects. Instead, a few basic constructors provide for a form of Object-Based Programming (that is, objects but no inheritance). The language is quite crude: the basic syntax reduces to half-a-dozen constructors. To help in writing common programming patterns, a few derived constructors are available. This talk introduces TyCO by example, rather than explaining the language first and giving examples second.
2 Maio 2001.
Michel Wermelinger. Reconfiguração Dinâmica em CommUnity: Linguagem e Semântica. É apresentado um formalismo baseado em regras de reescrita de grafos para especificar alterações a sistemas descritos por configurações de componentes escritos em CommUnity, uma linguagem de desenho paralela. De seguida é introduzida uma linguagem mais adequada a descrever esse processo, sendo a semântica dos comandos básicos dada pelas regras de reescrita.
18 Abril 2001.
Davide Sangiorgi. Coinductive techniques based on bisimulation. The most popular method for establishing bisimilarities results is to exhibit bisimulation relations. I will discuss generalisations of the method aimed at reducing the size of the relations to exhibit and hence relieving the proof work needed to establish bisimilarity results. The core of the talk is based on the paper ``On the bisimulation proof method , D. Sangiorgi, journal of MSCS, 8, 1998.'' I will also discuss more recent developments, including: the applications of the new techniques to functional languages (especially the work of Soren Lassen) and to process calculi for cryptography (Boreale, De Nicola, and Pugliese), their implementation and their application in mechanical verification of infinite-state-space processes (Hirschkoff, Roeckl), their use in the prove of decidability results for bisimilarity on infinite graphs (Caucal).
11 Abril 2001.
António Ravara. Distributed pi-calculus revisited. Part II.
28 Março 2001.
António Ravara. Distributed pi-calculus revisited. We investigate a core asynchronous distributed pi calculus, sdpi, which constitutes the base of several proposals of pi-calculus idioms with explicit notions of locality and with primitives for process migration. The calculus has a distributed lexical scoping mechanism that rules remote communication and process migration, hence migration primitives are superfluous. We compare sdpi with the Dpi calculus of Hennessy and Riely, defining ``good'' mutual encodings; and develop a type system for sdpi, based on the system of Amadio et alia, such that processes are typable by one system if and only if their encoding is typable by the other.
21 Março 2001.
Antónia Lopes. Apresentação preliminar (e experimental) do tutorial "Mathematical Foundations for Software Architecture" a ser apresentado no ETAPS'01.
1 Fevereiro 2001.
Luís Caires. A specification logic for concurrent open systems. We present MSL, a specification logic for generic concurrent open systems with Milner-style mobility. We will also show how MSL supports reasoning about interesting aspects of such systems, like structure, creation of new entities, local names, and their dynamics.
25 Janeiro 2001.
C. Caleiro. Distributed Temporal Logics (DTLs). We present two logics designed for the specification of distributed information systems, with emphasis on communication among sites. The lower-level DTL D0 offers features that are easy to implement but awkward to use for specification, while the higher-level DTL D1 offers convenient specification features that are not so easy to implement. We show that D1 specifications may be automatically translated to D0 in a sound and complete way. In order to prove soundness and completeness, we define our translation as a simple map of institutions. In the same lines, we also provide a proof of decidability of the validity problem for D1 by means of a suitable representation in Linear Temporal Logic (LTL). Complexity bounds for the decision problem for D1 are thus smoothly obtained from well known results for LTL. By further exploring this representation, we also prove that D1 is "trace-consistent"and hence that efficient model-checking for D1 is possible. Our results may be useful for making implementation platforms like CORBA more easily accessible by providing high-level planning and specification methods for communication.
14 Dezembro 2000.
Pedro Resende. Independência, causalidade e estruturas concorrentes em quantales. Nesta apresentação informal discuto os quantales (reticulados completos equipados com uma multiplicação associativa e distributiva sobre os supremos do reticulado) enquanto modelos de computação sequencial e apresento noções de estrutura concorrente em quantales, as quais permitem expressar noções típicas da chamada "concorrência verdadeira", como independência e causalidade, conduzindo de uma forma natural a uma noção de paralelismo invariante para refinamentos. As estruturas concorrentes formam estrutura adicional sobre um quantale, tal como por exemplo a topologia de um espaço topológico representa estrutura adicional sobre um conjunto. Deste modo os quantales com estruturas concorrentes podem ser encarados como "espaços de computação concorrente", resultantes de enriquecer com mais estrutura os "espaços de computação sequencial" que correspondem à estrutura habitual de quantale. Dou exemplos de quantales com estruturas concorrentes obtidos a partir de estruturas de eventos, e também de outros obtidos a partir de espaços topológicos, onde a noção de paralelismo está intimamente associada à dimensão do espaço.
7 Dezembro 2000.
António Branco. Natural negation. Segunda parte da apresentação de 23 Novembro 2000.
30 Novembro 2000.
Francisco Martins. Computations with the Immune System. The immune system is a highly intricate system capable of very complex pattern matchings. We explore the immune system as a biological metaphor applicable to computation and present a mathematical model of the immune system together with some experimental results.
23 Novembro 2000.
António Branco. Natural negation. Natural negation presents many challenging puzzles. In a oversimplied account of these challenges, one could underline the following two striking points: A single semantic negation may be entertained by the occurence of multiple negative forms:

Ninguem viu nada/
No one saw anything
Nem nunca ninguém disse nada a ninguém/
Never anyone said anything to anyone

A semantic negation may be entertained by no occurrence of any negative form:

Se Kennedy tivesse um carro blindado, teria
saído de Dallas com vida/
If Kennedy had a bullet proof car, he would
be alive when leaving Dallas.
(But) Kennedy had no bullet proof car.

For the first case, mainstream accounts tend to split into two views: (i) no negative expression expresses negation: single semantic negation is expressed by a phonetically null operator; (ii) all negative expressions express negation: multiple negations are factorized into a single one. The explicative appeal of these solutions is reduced: one ends up just rephrasing the empirical facts in terms of special-purpose stipulative mechanisms. In this talk, I would like to introduced you to a third type of solution I am working in, which is being developed, among other things, in our Nexing project. In this approach, downwards monotonicity properties are shown to play a decisive role in natural language.

16 Novembro 2000.
Vasco Thudichum Vasconcelos. Máquinas para interpretar cálculos de processos. Cálculos de processos constituem, cada vez mais, o núcleo de linguagens de programação concorrentes. Vem equipados com uma semântica operacional, mas esta semântica não se adapta facilmente ao hardware que temos sobre a secretária e no colo. Apresento uma série de máquinas para interpretar cálculos de processos, cada vez mais perto do hardware que todos temos, cada vez mais longe do cálculo original. [Trabalho em parceria com L. Lopes e F. Silva.]
9 Novembro 2000.
Isabel Nunes. Durative Timed Automata with Deadlines (DTAD's). We propose an extension of timed automata (Alur and Dill), namely of timed automata with deadlines (Sifakis and Yovine), in order to explicitly represent the duration of actions. The word duration denotes not only the real-time duration (units of time) but also the fact that the state in which an action begins execution is not necessarily the same in which it ends. This implies that other concurrently executing actions can interfere insofar as they can modify the state while the action is executing. A DTAD is a real-time extension of a (untimed) durative automaton; this extension is compositional in the sense that a DTAD that is obtained as the extension of the composition of untimed durative automata can also be obtained as the composition of the DTAD's obtained as extensions of those untimed components.
2 Novembro 2000.
Antónia Lopes. High-Order Connectors. The ability to construct architectural connectors in a systematic and controlled way has been argued to promote reuse and incremental development, e.g., as a way of super-posing, `a la carte, services like security over a given com-munication protocol. Towards this goal, we present a notion of high-order connector, i.e., a connector that takes con-nectors as parameters, for superposing coordination mech-anisms over the interactions that are handled by the con-nectors that are passed as actual arguments. [Joint work with Michel Wermelinger and José Luiz Fiadeiro.]
26 Outubro 2000.
José Luiz Fiadeiro. Usando o exemplo das pilhas, ilustram-se alguns problemas da técnica de "desenho por contrato" promovida pelo B.Meyer e sugerem-se algumas soluções
27 Setembro 2000
Pedro Rodrigues. iContract - Contratos em Java. O iContract é uma ferramenta, desenvolvida em Java e para Java (versão 2), que permite a verificação de contratos em tempo de execução. Nesta apresentação procurarei expor o modo como a ferramenta pode ser usada, as suas potencialidades, as suas limitações e alguns dos seus 'bugs'.
8 Setembro 2000
Elaine Pimentel, Universidade Federal Minas Gerais, Brasil. Linear Logic as a Framework for Specifying Sequent Calculus. In recent years, intuitionistic logic and type systems have been used in numerous computational logic systems as frameworks for the specification of natural deduction proof systems. As we shall illustrate here, linear logic can be similarly used to specify the more general setting of sequent calculus proof systems. We shall present several example encodings of sequent calculus proof systems using the Forum presentation of linear logic.
21 Março 2000.
Vasco Thudichum Vasconcelos. Quatro máquinas de passagem por valor. Passagem por valor é a estratégia seguida por grande parte das linguagens de programação. Ainda alguém se lembra da máquina ISWIM utilizada por Peter Landin nos anos 60 para descrever características de linguagens de programação? e da versão simplificada SECD de Gordon Plotkin dos anos 70? Apresento a correspondência operacional entre o cálculo-lambda com a estratégia adequada, a máquina SECD, e duas máquinas baseadas no cálculo-pi.
15 Março 2000.
Pedro Rodrigues. Verificação de propriedades em redes neuronais (parte 2). Nesta apresentação vamos terminar a exposição iniciada no último encontro de Quarta-Feira, partindo da adequação do sistema de tableaux à verificação de propriedades em redes neuronais e terminando com a apresentação de uma forma possível de automatizar o processo de prova para redes inteiras.
1 Março 2000.
Pedro Rodrigues. Verificação de propriedades em redes neuronais. Em meados da década de 90, Hava Siegelmann propõe um novo modelo de computação, a "Artificial Recurrent Neural Network" (rede neuronal recorrente), e demonstra que o seu poder computacional é super-Turing. A par deste resultado, Hava Siegelmann estabelece ainda a equivalência entre o novo modelo de computação e múltiplos outros modelos analógicos, também de poder computacional super-Turing, lançando as bases de uma teoria computacional alternativa. Nós procuramos contribuir para o corpora disciplinar desta teoria computacional alternativa ao explorar a aplicação de métodos formais na verificação de propriedades em redes neuronais recorrentes. Para tal, partimos de um sistema de verificação desenvolvido por Bradfield para sistema infinitos, simplificamo-lo, preservando a sua capacidade de prova, e mostramos que o sistema resultante é adequado à verificação de propriedades em redes neuronais recorrentes. A par desta adequação, mostramos ainda como é possível automatizar o sistema de prova para uma subclasse de redes neuronais recorrentes, as redes inteiras.
2 Dezembro 1999.
José Luiz Fiadeiro. Towards a verification logic for rewriting logic. We present a first step towards the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and show its possibilities by means of two simple examples.
25 Novembro 1999.
Vasco Thudichum Vasconcelos. Secure Information Flow as Typed Process Behaviour. We propose a new type discipline for the pi-calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A behavioral notion of types capturing causality of actions plays an essential role for ensuring safe information flow in diverse interactive behaviours, making the calculus powerful enough to embed known calculi for type-based security. We illustrate its use as a tool for programming language analysis by a sound embedding of a secure multi-threaded imperative calculus of Volpano and Smith. [Joint work with Kohei Honda (Queen Mary and Westfield College), and Nobuko Yoshida (University of Leicester).]
18 Novembro 1999.
Manuel Campagnolo, Santa Fe Institute. Analog Computation of Subrecursive Functions. We analyze some related models of analog computation evolving in continuous time. We show that the class of functions, G, computed by Shannon's General Purpose Analog Computer (GPAC) is not closed under iteration, but a simple extension of it is. In particular, if we relax the definition of GPAC slightly to include unique solutions to boundary value problems then the resulting class, G+T, is closed under iteration. Furthermore, G+T includes all primitive recursive functions and has the additional closure property that any function computable by a Turing machine in time in G+T is also in G+T. Then, we define a subclass of G+T, which we call L+T, where the integration in GPAC is restricted to linear integration. We show that L+T gives an analog characterization of the class of elementary functions. Thus we claim that natural models of realistic analog computation correspond to natural subsets of the recursive functions.
4 Novembro 1999.
José Luiz Fiadeiro. Vou apenas fazer uma reportagem sobre o que se passou no UML'99.
21 Outubro 1999.
Antónia Lopes, Isabel Nunes. Data and State Model of a Simple OO language as proposed in [Poetzsch-Heffter, Arnd , "Specification and verification of Object-Oriented Programs", Habilitationsschrift].
2 Junho 1999.
Andrzej Tarlecki, Institute of Informatics, Warsaw University, and Institute of Computer Science, Polish Academy of Sciences Warsaw. Architectural specifications in CASL. One of the most novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of CASL specifications will provide the setting for a presentation of the rationale behind architectural specifications. This will be followed by some details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process. [Joint work with Michel Bidoit and Don Sannella.]
28 Abril 1999.
Luis Mandel, FAST eV (Research Institute for Applied Software Technology). On the Expressive Power of OCL. We examine the expressive power of OCL in terms of navigability and computability. First the expressive power of OCL is compared with the relational calculus. Then an algorithm computing the transitive closure of a binary relation --operation that cannot be encoded in the relational calculus-- is expressed in OCL. Finally the equivalence of OCL with a Turing machine is pondered. [Joint work with María Victoria Cengarle.]
21 Abril 1999.
María Victoria Cengarle, University of Munich. Rewriting theories embedded in temporal logic. A rewrite logic institution and a temporal logic institution are presented together with sound proof calculi and a translation mechanism from the first logic into the latter one that allows to view rewrite theories as implementation of temporal logic specifications thus facilitating verification. Moreover a theory-building operator is defined that allows synchronization of rewrite theories wrt pairs of rewrite rules. The novelty of this approach is twofold: the program result of synchronization is not explicitly calculated and reducts determine the class of models of a combined program.
14 Abril 1999.
Vasco Thudichum Vasconcelos. Encoding the call-by-value lambda-calculus into the pi-calculus. On sequentiality and concurrency, on the lambda-calculus and the pi-calculus, on compiling the former into the latter, and on the need to protect sequential computations from the permissive behaviour of concurrency.
24 Março 1999.
Björn Victor, Uppsala University. Solos in Concert - fusion at work. A technical expressiveness result is presented: in a subcalculus of the fusion calculus without prefix or summation, we use two different encodings to show that it can express both action prefix and guarded summation. One encoding gives a strong correspondence but uses a match operator; the other yields a slightly weaker correspondence but uses no additional operators. We relate these results to similar work in the pi-calculus. [Joint work with Cosimo Laneve.]
17 Março 1999.
Bernie Cohen, City University, London . Modelling Services and Agents. We use examples of 'feature interaction', in telecoms and elsewhere, to demonstrate the kinds of inconsistency that can, and do, arise among service specifications and their implementations, and to illustrate some of the theoretical problems that still face the OO and distributed systems communities, despite the recent developments in UML, CORBA, etc.
10 Março 1999.
Ana Moreira. Formal specifications from informal requirements. Building a formal specification from informal requirements is difficult. To simplify this, we first build a formal user-centred model that specifies behaviour from the viewpoint of the requirements. The resulting model is then used to construct a formal object-oriented requirements specification, i.e. a system-centred model. The whole process uses a subset of UML as a steping stone to build the final formal specification.
3 Março 1999.
António Ravara. What is TyCO after all? To understand the nature of TyCO we discuss possible encodings of polyadic TyCO into monadic TyCO, and then into some asynchronous pi-calculus. [Joint work with Uwe Nestmann.]
10 Fevereiro 1999.
Michel Wermelinger. Reescrita de Arquitecturas CommUnity. É apresentado um método para especificar reconfigurações de arquitecturas de programas CommUnity com estado, usando regras de reescrita condicionais baseadas na abordagem algébrica de gramáticas de grafos (de Ehrig et al).
3 de Fevereiro 1999.
Pedro Resende. Bisimulation and HML for image-infinite systems. We extend the well known modal characterization of bisimulation of Hennessy and Milner by studying conditions, weaker than image-finiteness, under which bisimulation coincides with logical equivalence.
27 de Janeiro 1999.
Salvador Pinto Abreu. University of Evora's Integrated Information System. We present the University of Evora's Integrated Information System (SIIUE), which is meant to model most of the information necessary for the management and day-to-day operation of an institution such as a public University. SIIUE is centered around a logic-based representation of all intervenients and processes, which is used to generate the more efficient and specific representations for the actual use -- this includes extended SQL, PHP3 and Java code generation. SIIUE also interacts with an etherogenous set of partial information systems, both to supply and collect information.
9 Dezembro 1998.
Rui Bastos. O estado actual da linguagem TyCO (TYped Concurrent Objects): sintaxe, semântica, sistema de tipos, implementação e compilação.
2 Dezembro 1998.
António Ravara. Communication Errors in the Pi-Calculus are Undecidable. We present an undecidability proof of the notion of communication errors in the polyadic pi-calculus. The demonstration follows a general pattern of undecidability proofs -- reducing a well-known undecidable problem to the problem in question. We make use of an encoding of the lambda-calculus into the pi-calculus to show that the decidability of communication errors would solve the problem of deciding whether a lambda term has a normal form. [Joint work with Vasco T. Vasconcelos.]
25 Novembro 1998.
Antónia Lopes. Using Explicit State to Describe Architectures. In order to achieve higher levels of abstraction in architectural design, we investigate extensions to parallel program design based on the use of explicit state variables to accommodate the action-based discipline of interaction that is typical of architecture description languages. Our study focus on primitives that support non-determinism, choice and fairness in guarded-command based languages, and on refinement principles that are compositional with respect to interconnection.
11 Novembro 1998.
Vasco Thudichum Vasconcelos. Distribution and Mobility in Process Calculi. We propose a simple model of distribution for mobile processes, independent of the underlying calculus. Conventional processes compute within sites; inter-site computation is achieved by message sending and object migration, both obeying a lexical scope. We focus on the semantics of networks, on programming practice, and on physical realisation with current technology. [Joint work with Luís Lopes and Fernando Silva.]
4 Novembro 1998.
Nuno Barreiro. A estabilidade foi introduzida por G.Berry nos anos 70 e é um dos ingredientes principais da semântica denotacional da lógica linear. Um outro ingrediente é a interpretação dos conectivos exponenciais, que, na semântica usual, é feita com conjuntos. Nessa interpretação é possível caracterizar a a implicação intuicionista como um espaço de funções estáveis. Mas existem outras formas de interpretar os conectivos exponenciais, nomeadamente com multiconjuntos, tendo esta ultima intepretação a propriedade universal de ser o comonóide comutativo livre dum grafo. Não é no entanto possível de, neste quadro, descrever a implicação intuicionista como um espaço de funções estáveis. Dar-se-á uma generalização do conceito de estabilidade que permite estabelecer, para o caso da interpretação com multiconjuntos, uma contrapartida funcional à implicação intuicionista. [Trabalho em parceria com Thomas Ehrhard (IML/CNRS).]
28 Outubro 1998.
Narciso Marti Oliet, Universidade Complutense de Madrid. Metalevel Computation in Maude. Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way, and makes possible many advanced metaprogramming applications, including user-definable strategy languages, language extensions by new module composition operations, development of theorem proving tools, and reifications of other languages and logics within rewriting logic.
21 Outubro 1998.
Pedro Rodrigues. Verificação de propriedades de redes neuronais. Partindo do trabalho de Bradfield respeitante à verificação de propriedades temporais de sistemas de transição etiquetados, procura-se adaptar a solução encontrada a uma determinada classe de redes neuronais. Nesse esforço de adaptação, produz-se uma extensão da linguagem utilizada para descrição das propriedades, o cálculo-mu modal proposicional, "reformula-se" a técnica utilizada na verificação, o método de tableau, e procura-se identificar classes de redes neuronais onde a verificação possa ser completamente automática.
7 Outubro 1998.
António Branco. Processamento de referência e quantificação fásica: Existe um conjunto de generalizações acerca de restrições para o processamento de referência nas línguas naturais. Apresentarei uma reconstrução formal dessas generalizações à custa de mecanismos de quantificação fásica. Discutirei as implicações e vantagens deste deslocamento epistémico para os modelos computacionais e cognitivos do processamento de referência. Em atenção aos mais preocupados com a rentabilização do trabalho académico, sera´ reservado algum tempo para uma dilucidação da utilidade prática e valor comercial de modelos eficazes de processamento de referência.
30 Setembro 1998.
Paulo Carreira. Verificação de especificações OBLOG. A distribuição do esforço empregue durante o ciclo de desenvolvimento de software é 40-20-40 respectivamente para Análise e Desenho, Codificação, Teste e Integração. A disponibilização de ambientes de desenvolvimento que aumentem a qualidade da Análise e/ou diminuam o esforço da fase de Testes é uma prioridade. Neste contexto, ferramentas baseadas em métodos formais como o OBLOG tem sido empregues com algum sucesso. Uma das vertentes do uso dos métodos formais é a possibilidade de realizar verificação automática de propriedades de programas recorrendo a uma técnica denominada verificação de modelos. Em fase de estudo estão a aplicabilidade desta técnica, as suas limitações e a interface com ferramentas existentes.
29 Abril 1998.
António Ravara. An object calculus with implicit communication. We propose an object-type algebra that characterises the semantics of objects in a concurrent setting where the communication is asynchronous, but where the types provide an internal (and synchronous) view of the objects that inhabit them. These ideas, along with the algebraic laws, are based on a notion of bisimulation that is unlike other notions in the literature.
25 Março 1998.
António Ravara. A type algebra for concurrent objects. We propose a new notion of error-process and a new notion of types to cope with non-uniform service availability in concurrent objects. We develop a type system that ensures the absence of run-time errors and local deadlocks for typable processes.
11 Março 1998.
João Araújo. Metamorphosis: Um método integrado de análise e especificação de requisitos orientado a objectos. O objetivo deste trabalho é integrar métodos formais e semiformais OO na atividade de especificação de requisitos do processo de engenharia de requisitos. Além de um modelo OO, o método também incorpora uma linguagem de especificação formal, no caso é Object-Z. Estas duas abordagens são combinadas através de um conjunto de regras para transformar uma representação em outra. Um toolset dá suporte tanto à modelagem quanto ao processo de tradução.
4 Março 1998.
Vasco Thudichum Vasconcelos. Processos, Funções, Estruturas de Dados. Do mesmo modo que ninguém escreve programas funcionais directamente no cálculo-lambda, ninguém vai querer escrever programas concorrentes no cálculo-pi. Apresento algumas comodidades que visam tornar o cáculo-pi (ou melhor TyCO) numa (quase) linguagem de programação. A adição de novos construtores - essencialmente funções e estruturas de dados - segue uma metodologia: os novos construtores são compiláveis em pi, e possuem regras de tipificação extraídas do método de compilação.
18 Fevereiro 1998.
F. Miguel Dionísio. Composition of Hierarchic Default Specifications. The classical theory of Institutions from Burstall and Goguen provides the formal grounds for describing structuring operations that allow to build specifications from smaller specification modules. In this talk a generalization of this abstract specification theory to specifications including "defaults" is presented.
11 Fevereiro 1998.
Luís Caires. We discuss a logical framework for specifying and reasoning about (systems of) concurrent processes (objects) with mobility features. The intended models of the logic are certain variants of the action calculi of Milner, where the modelled processes interact under data domains constructed upon dynamically extensible signatures.
14 Janeiro 1998.
Luís Lopes. In this talk we present a self-contained abstract machine for process (object) calculi based languages. We focus on the machine architecture, the instruction set, and the "byte-code" assembler and interpreter. Some performance results are compared to a previous C implementation and other existing languages such as Pict and Haskell.
17 Dezembro 1997.
Manuel Lameiras Campagnolo. It is known that the class of differentially algebraic (d.a.) functions is exactly the class of functions computed by Shannon's General Purpose Analog Computer and that the class of d.a. functions is strictly included in the class of recursive functions. Moore's extension of Shannon's GPAC computes the class of R-recursive functions which includes all recursive functions but also non-recursive functions. However, Moore's model has an unphysical operator. Here, we introduce a new model of computation which computes a subclass of R-recursive functions. We show that it is more powerful than Shannon's GPAC and that the simulation of an arbitrary Turing machine is possible in it. Moreover, we argue that this new model of analog computation is physically realizable.
10 Dezembro 1997.
Luis Andrade. The Oblog97 approach to the design and development of Reactive Information Systems. Extensions of the this approach in order to deal with proactive systems. UML has been presented as an industry effort to create a new general purpose standard graphical notation for Information Systems specification. Besides its merit to create an universal notation, and having in mind that its use is mainly focused on defining Information Systems which would be somehow implemented, it is mandatory to provide this standard with a rigorous semantic interpretation for each concept (language constructor) as well as well defined mappings to key information technologies, namely databases, transactions, concurrency, oopl, 3gls, etc. This talk presents a rigorous set of concepts for object specification and how they can be rigorously used to give a semantic interpretation for a subset of the UML notation, which is claimed to be sufficient for the specification of reactive systems. It is advocated that this approach drops the major mismatching between models or paradigms, improving the productivity and quality for large scale projects. The successful use of this approach in the development of a mission critical Portuguese bank project is reported.
19 Novembro 1997.
Pierre-Yves Schobbens. Real-time logics. In this talk we consider the expressiveness and complexity of several real-time logics belonging to the families of: - explicit time logics: where time is represented by a specific sort. For decidability, we consider only monadic logics: TML1, TML2, RTML2, LD. - metric temporal logics: where time is implicit in modalities. We consider SCL, MITL, MTL. - real-time automata: though they are not usually considered as a logic, automata have similar properties: (non-)decidability, closure under conjunction, disjunction, negation, etc. We consider Timed Automata and State Clocks Automata. These logics come in several variants: inclusion of past time, reflexive or irreflexive future, second-order, etc. Our aim is to place them in the hierarchies of expressiveness and complexity.
5 Novembro 1997.
Michel Wermelinger. Towards a Chemical Model of Software Architecture Reconfiguration. In this talk I will briefly review the Chemical Abstract Machine (CHAM) and how it was used by Inverardi et al to describe the computational behaviour of (static) software architectures. I will also present Le Metayer's paper on using graph grammars to describe architectural styles and evolution. Finally, it will be shown how the CHAM might be used for the same purpose and how it might represent different approaches to reconfiguration taken in Distributed Software Engineering. This work is still very sketchy and therefore any comments will be appreciated.
29 Outubro 1997.
Jaime Ramos. We start by shortly presenting the traditional situation calculus (SC). Within SC, we discuss the usual notion of state, namely its unsuitability for system specification. To overcome this limitation, we propose an extension of SC that embodies a more suitable notion of state, the situation and state calculus (SSC). We compare SSC with several temporal logics (propositional linear temporal logic and branching temporal logic).
15 Outubro 1997.
Vasco Thudichum Vasconcelos. One can write a Prolog interpreter with three lines of Prolog; one can write an Oberon compiler with twelve hundred lines of Oberon; why shouldn't one be able to write a Pi interpreter with six lines of Pi? (or: on functions, processes, data types, and self-interpreters for the pi-calculus).
8 Outubro 1997.
António Ravara. A type algebra for concurrent objects: syntax and a first aproximation to semantics.
24 Setembro 1997.
João Neto. Sobre como implementar algoritmos arbitrariamente complexos em redes neuronais (representadas por sistemas dinâmicos de primeira ordem) utilizando o interface de uma linguagem paralela de alto nível.
17 Setembro 1997.
Antónia Lopes. I. Como decorreu o International Symposium Compositionality - The Significant Difference. II. Abordagem composicional à semântica de sistemas abertos. Preservação, reflexão e composição de propriedades.
23 Julho 1997.
Vasco Thudichum Vasconcelos. I. Como decorreu o 24th International Colloquium on Automata, Languages and Programming. II. We introduce basic language constructs and type disciplines for structured communication-based concurrent programming, which are suitable for high-level description of applications in the networked environments. The constructs, while easily translatable into the summation-less asynchronous pi-calculus, allow programmers to organise their programs as a combination of multiple flows of reciprocal interactions in a disciplined way, subsuming the preceding constructs such as method invocation, remote procedure call, and rendez-vous. Two typing systems are introduced, one for verifying compatibility of communication patterns and another ensuring a certain form of deadlock freedom in interaction, both utilising the structuring constructs in an essential way. [Joint work with Kohei Honda.]
2 Julho 1997.
Luís Lopes. Uma máquina abstracta para o cálculo de objectos proposto por V. Vasconcelos. Descrição da sintaxe abstracta e regras de redução. Relação com o cálculo de objectos original e outras máquinas abstractas propostas (e.g., Pict, Oz).
25 Junho 1997.
Luís Caires. Elsewhere we have proposed Lpi, a simple meta language for defining executable specifications of concurrent computations. In this talk, it will be sketched how a simple syntax-directed translation technique into Lpi can be used to execute temporal logic specifications of concurrent objects.
18 Junho 1997.
Michel Wermelinger. Apresentarei uma versão preliminar do Mobile COMMUNITY, uma variante do COMMUNITY (linguagem baseada no UNITY) que permite descrever interacções temporárias. A linguagem não foi alterada, apenas os morfismos entre programas. Dados os programas e as condições sob as quais interagem, apresentarei os conectores que permitem descrever a arquitectura do sistema. Será feita uma comparação com o Mobile UNITY de Gruia-Catalin Roman et al.
11 Junho 1997.
António Ravara. We present a new type system for TyCO, a name-passing calculus of concurrent objects. The system captures dynamic aspects of objects' behaviours, namely non-uniform service availability of active objects. The notion of processes without errors is loosened, demanding only weak fairness in the treatment of messages.
12 Março 1997.
Antónia Lopes. Sobre como decorreu o Dagstuhl-Seminar 9710: Logic for Systems Engineering.
5 Março 1997.
Marcos Mota Costa. Inductive Logic Programming. Apresentação do andamento do projeto de Pós-doutoramento. Visão geral de ILP. Generalização e especialização. Sistema de tableau para ILP.
26 Fevereiro 1997.
António Rito Silva. The current status of DASCo (Development of Distributed Applications with Separation of Concerns) project will be presented. DASCo emphasizes separation of concerns at both, problem and solution spaces. Two pattern languages, addressing partitioning and concurrency problems, were designed. At the solution space, the development process is supported by a three-layered framework providing design solutions for concurrency, synchronization, recovery, replication, naming, configuration and communication concerns. The presentation overview the DASCo approach and focus, afterwards, on the concurrency problem and respective solutions.
19 Fevereiro 1997, 2pm.
Nobuko Yoshida. Graph Types for Mobile Processes. While types for name passing calculi have been studied extensively in the context of sorting of polyadic pi-calculus, the type abstraction on the corresponding level is not possible in the monadic setting, which was left as an open issue by Milner in 1992. We solve this problem with an extension of sorting which captures dynamic aspects of process behaviour in a simple way. The construction is general enough to be extendable to encodings of calculi with more complex operational structures.
5 Fevereiro 1997.
Pedro Resende. Sistemas tropológicos em concorrência e especificação. Tópicos: quantales e observações finitas; sistemas tropológicos; aplicações à semântica e especificação de sistemas concorrentes.
29 Janeiro 1997.
Vasco Thudichum Vasconcelos. Sobre como decorreu o 24th Annual ACM Symposium on Principles of Programming Languages, o 4th International Workshop on Foundations of Object-Oriented Languages, e o Seminar on High-Level Concurrent Languages.
22 Janeiro 1997.
António Horta Branco. Maximization of content/form ratio and its universal limits. Ongoing author's research on a performance based approach to reference resolution at the syntax-semantics interface in natural language computational grammars will be presented.
15 Janeiro 1997.
Edward Hermann Haeusler. Uma Abordagem Modelo-Categorica para a Definição de Quantificadores: Aplicação a Quantificadores Multiplicativos. Este trabalho apresenta uma abordagem abstrata para a definição de quantificadores como generalizações de operadores proposicionais de uma "lógica" . Esta "lógica" deve possuir um modelo algébrico (completo e correto) e uma apresentação em dedução natural (proposicional). O modelo associado reune características de modelos para a lógica de primeira ordem com modelos categóricos baseados em teoria da prova. Mostra-se que os quantificadores multiplicativos podem ser modelados nesta abordagem.
8 de Janeiro de 1997.
Luís Caires. Semântica denotacional baseada em redes de prova para uma linguagem lógica concorrente.
11 Dezembro 1996.
Workshop MAGO: Modelação de Agentes em Organizações. Sessão Especial no IFM sala B101.
Luís Antunes. Alguns Ângulos dos Valores.
Pedro Ramos. Uma Lógica Deontica para o Diagnóstico de Desenho de Processos.
Filipe Santos. A Modal Action Logic Based Framework for Organization Specification and Analysis.
4 Dezembro 1996.
João Barreto. Replicaçäo activa - panaceia da tolerância a falhas em sistemas distribuídos!? Alguns tópicos sobre o trabalho desenvolvido por R.Fleming e P.Harry (HP Labs). Sobre a I&D nos laboratórios industriais - o funcionamento e ambiente dum super-lab.
27 Novembro 1996.
Isabel Nunes. Uma generalização de sistemas de transicções e a lógica multimodal correspondente são propostos, como forma de dar semântica a programas no paradigma de programação proposto pelo Prof. W.M.Turski, no qual as acções têm duração e, por isso, podem interferir.
20 Novembro 1996.
António Ravara. Um sistema de tipos para o Typed Calculus of Objects que captura aspectos do comportamento dos processos, e alarga a classe de processos tipificáveis. Os tipos são interpretados por fórmulas temporais.
13 Novembro 1996.
Pedro Ramos. Diagnóstico de Processos em Organizações. Utilização de técnicas formais de auxílio ao diagnóstico. A abordagem é baseada na teoria clássica de Diagnóstico (Reiter) e é suportada por lógica deôntica.
6 Novembro 1996.
Antónia Lopes. Apresentação de uma extensão da abordagem categorial do desenho de sistemas reactivos proposta em [Fiadeiro e Maibaum 96, "Categorical Semantics of Parallel Program Design", Science of Computer Programming]. Demonstração de como esta extensão alarga o âmbito de aplicação da abordagem, em particular, a formalismos "action-based" que distinguem não-determinismo externo e interno.
30 Outubro 1996.
Michel Wermelinger. Configuração dinâmica de sistemas distribuídos no caso particular do trabalho desenvolvido pela equipa de Jeff Kramer do Imperial College. Parte II.
23 Outubro 1996.
Michel Wermelinger. Configuração dinâmica de sistemas distribuídos no caso particular do trabalho desenvolvido pela equipa de Jeff Kramer do Imperial College. Parte I.
16 Outubro 1996.
Carlos Paredes. Sobre como decorreu o OOPSLA 96, e minha apresentação num dos workshops da conferência.