Recent Publications

Ridder A, Posadas F, Campos JC.  2005.  Technical Guide for the Visualiser Component.
Campos JC.  2004.  Interactors as Boundary Objects. Abstractcamposch01ws.pdf

Too often software engineers see the user interface as a last layer that must be placed on top of the functional (or business logic) layer in order (simply?) to enable users access to its functionality. This vision rests on the assumption that all the application’s logic is at the functional level, and is independent of the user interface. The user interface then is simply a information transmission layer between the user and the “application” (i.e., the functional layer).

Cunha A, Pinto JS.  2004.  Point-free Program Transformation. Abstractpuretr040203.pdf

Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the introduction of accumulating parameters, can be implemented using calculation through the use of the fusion (or promotion) strategy. In this paper we revisit this transformation method, but, unlike most of the previous work on this subject, we adhere to a pure point-free calculus that emphasizes the advantages of equational reasoning. We focus on the accumulation strategy initially proposed by Bird, where the transformed programs are seen as higher-order folds calculated systematically from a specification. The machinery of the calculus is expanded with higher-order point-free operators that simplify the calculations. A substantial number of examples (both classic and new) are fully developed, and we introduce several shortcut optimization rules that capture typical transformation patterns.

Cunha A.  2003.  Recursion Patterns as Hylomorphisms. Abstractdi-pure-031101.pdf

In this paper we show how some of the recursion patterns typically used in algebraic programming can be defined using hylomorphisms. Most of these definitions were previously known. However, unlike previous approaches that use fixpoint induction, we show how to derive the standard laws of each recursion pattern by using just the basic laws of hylomorphisms. We also define the accumulation recursion pattern introduced by Pardo using a hylomorphism, and use this definition to derive the strictness conditions that characterize this operator in the presence of partiality. All definitions are implemented and exemplified in Haskell.

Cunha A, Barros J B.  2003.  Towards Utility-based Programming. Abstractuspl.pdf

Many programs have an objective that can be precisely stated as the maximization of a function defined over its local variables. This is the case of utility-based software agents, which are reactive entities that try to maximize their welfare, usually accessed by an utility function. This paper introduces a programming language suitable for explicit programming with utility functions. Starting from a standard concurrent programming language, we added primitives to allow the parametrization of each process with an utility function that should be maximized. For the moment, using techniques of Markov decision problems, we can compile sequential programs, written in a restricted version of this new language, into equally behaved programs written in the original one. Major problems in developing such utility-based programming language are the need to compare the utility of infinite executions or the need to deal with uncertainty.

Campos JC, Harrison M.  1999.  From Interactors to SMV: A Case Study in the Automated Analysis of Interactive Systems. Abstractycs-99-317.pdf

Recent accounts of accidents have drawn attention to problems that arise in safety critical systems through “automation surprises”. A particular class of such surprises, interface mode changes, may have significant impact on the safety of a dynamic interactive system and may take place implicitly as a result of other system action. Formal specifications of interactive systems may provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an interactor based specification may have as a partial model of an interactive system, so that mode consequences might be checked early in the design process. We show how interactor specifications can be translated into the SMV model checker input language, and how we can use such specifications in conjunction with the model checker to analyse potential for mode confusion in a realistic case. Our final aim is to develop a general purpose methodology for the automated analysis of interactive systems, and, in this context, we show how the verification process can be useful by raising questions that have to be addressed in a broader context of analysis.

Moreno CB.  1996.  Indirect Calls: Remote invocations on loosely coupled systems. Abstract10.1.1.40.9706.pdf

Integration of Mobile computers into Worldwide networks is traditionally managed by hosting them into the fixed network. We argue that this approach excludes some important forms of interaction. We present a communication mechanism, suitable for developing applications that take advantage of transient connections. These communications can be supported by several transport mechanisms, including Email and plain file copying between non networked computers. 1 Introduction Future applications can be expected to follow two major trends, Mobility and Worldwideness. These two issues are strongly interrelated as Worldwide systems often experience disconnected operation under network partitions and Mobile computers are partially integrated (possibly hosted) into worldwide networks. A common scenario for the integration of mobile hosts (MHs) is based on a fixed worldwide network to which MHs connect from time to time, either by fixed or wireless links.

Moreno CB.  1995.  Synergetic state evolution under mobile computing. Abstract10.1.1.40.6574.pdf

The recent trend towards mobility and ubiquitous computing issued a new perspective over the traditional models of distributed computation. Observation of Human behavior, in particular the study of Human information interchange techniques and protocols presents a simple, yet fruitful, mean of gathering insight on the possible protocols for interaction among mobile hosts.This work will try to go one step further on the study of mobile interactions by leaving the usual semi-centralized approach to mobile computing. Instead of focusing on the reconciliation of mobile hosts with the networked support stations, we will study the possibility of progressive adjustments, both by a mobile host and a support station and between mobile hosts. 1 Introduction The recent trend towards mobility and ubiquitous computing issued a new perspective over the traditional models of distributed computation.

Campos JC.  1995.  GAMA-X - MIU Programmer's Manual. Abstractmiu_prog_man95.pdf

The GAMA-X system is a semi-automatic generator of assisted interfaces  . It aims at being an UIMS (User Interface Management System) for the Camila system  capable of providing an user interface that can be used at all levels of the application development cycle from the prototype to the nal implementation. The GAMA-X system is divided into two main modules the MGI (Interface Generation Module) and the MIU (User Interaction Module). The MGI generates an user interface specication or MIU specication from the computational layer specication The MIU creates an user interface based on the specication generated by the MGI. The MIU specications can be generated by the MGI or hand written from scratch In this manual we show with an example how to write the MIU specication.

Barros J B, Goguen J.  1995.  Semantics of Non-terminating Rewrite Systems using Minimal Coverings. Abstractprg118.pdf

We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of this minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non-termination systems to this minimal covering. These include the existence of normal forms for arbitrary rewrite systems, and their uniqueness for confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated with the rules when seen as equations. This extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders and then instantiate these to term rewriting systems.

Campos JC, Martins F.  1994.  Automatic Generation of User Interfaces at Prototype Level. Abstract

This report puts forward a software architecture aimed at providing tecnological support for User Interface design in the framework of a rigorous methodology for Interactive Systems development. Starting from the formal specification of the application layer, the methodology aims at the systematic development of the interactive system, with the main goal of creating high quality interfaces with a high degree of assistance to the user, error preventing features and contextual sensitivity. The proposed system, GAMA-X, offers an architecture for the systematic and semi-automatic development of this kind of interface, including tools that support the various steps of development. The architecture of the GAMA-X system is presented, with a special focus on the modules more closely related with the User Interface, as well as the description of a specification language for the Dialogue Controller. Some aspects about the communication between modules and about the presentation layer are also discussed.

Madeira F, Campos JC, Castro P, Martins F.  1990.  GAMA - Geração Automática de Modo Assistido.