Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
-
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.]
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
-
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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
-
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]
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
-
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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
-
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
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996
- 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.
Quick links:
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996