Type System for the ComponentJ Programming Language

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do grau de Mestre em Engenharia Informática.

A logical foundation for session-based concurrent computation

Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.

Type inference for conversation types

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

BIWiki - Using a Business Intelligence Wiki to Form a Virtual Community of Practice for Portuguese Master's Students

Web 2.0 software in general and wikis in particular have been receiving growing attention as they constitute new and powerful tools, capable of supporting information sharing, creation of knowledge and a wide range of collaborative processes and learning activities. This paper introduces briefly some of the new opportunities made possible by Web 2.0 or the social Internet, focusing on those offered by the use of wikis as learning spaces. A wiki allows documents to be created, edited and shared on a group basis; it has a very easy and efficient markup language, using a simple Web browser. One of the most important characteristics of wiki technology is the ease with which pages are created and edited. The facility for wiki content to be edited by its users means that its pages and structure form a dynamic entity, in permanent evolution, where users can insert new ideas, supplement previously existing information and correct errors and typos in a document at any time, up to the agreed final version. This paper explores wikis as a collaborative learning and knowledge-building space and its potential for supporting Virtual Communities of Practice (VCoPs). In the academic years (2007/8 and 2008/9), students of the Business Intelligence module at the Master's programme of studies on Knowledge Management and Business Intelligence at Instituto Superior de Estatistica e Gestao de Informacao of the Universidade Nova de Lisboa, Portugal, have been actively involved in the creation of BIWiki - a wiki for Business Intelligence in the Portuguese language. Based on usage patterns and feedback from students participating in this experience, some conclusions are drawn regarding the potential of this technology to support the emergence of VCoPs; some provisional suggestions will be made regarding the use of wikis to support information sharing, knowledge creation and transfer and collaborative learning in Higher Education.

Information flow analysis using data-dependent logical propositions

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

A type system for value-dependent information flow analysis

Information systems are widespread and used by anyone with computing devices as well as corporations and governments. It is often the case that security leaks are introduced during the development of an application. Reasons for these security bugs are multiple but among them one can easily identify that it is very hard to define and enforce relevant security policies in modern software. This is because modern applications often rely on container sharing and multi-tenancy where, for instance, data can be stored in the same physical space but is logically mapped into different security compartments or data structures. In turn, these security compartments, to which data is classified into in security policies, can also be dynamic and depend on runtime data. In this thesis we introduce and develop the novel notion of dependent information flow types, and focus on the problem of ensuring data confidentiality in data-centric software. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values. Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs. Namely programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields The main contribution of this work is an efficient analysis that allows programmers to verify, during the development phase, whether programs have information leaks, that is, it verifies whether programs protect the confidentiality of the information they manipulate. As such, we also implemented a prototype typechecker that can be found at http://ctp.di.fct.unl.pt/DIFTprototype/.

A type system for access control in an object-oriented language

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Analysis of support for modularity in object teams based on design patterns

Dissertação de Mestrado em Engenharia Informática

A qualitative assessment of modularity in CaesarJ components based on implementations of design patterns

Tese de Mestrado em Engenharia Informática

Model morphisms (MoMo) to enable language independent information models and interoperable business networks

MSc. Dissertation presented at Faculdade de Ciências e Tecnologia of Universidade Nova de Lisboa to obtain the Master degree in Electrical and Computer Engineering

Petri nets based components within globally asynchronous locally synchronous systems

Dissertação apresentada na Faculdade de Ciências e Tecnologias da Universidade Nova de Lisboa para a obtenção do grau de Mestre em Engenharia Electrotécnica e Computadores

Petri net model decomposition - a model based approach supporting distributed execution

Dissertação apresentada para obtenção do Grau de Doutor em Engenharia Electrotécnica, Especialidade de Sistemas Digitais, pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Time-domain optimization of amplifiers based on distributed genetic algorithms

Thesis presented in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the subject of Electrical and Computer Engineering

Service-oriented mobility of java code in web services-based architectures

Dissertação apresentada na Faculdade de Ciências e Tecnologias da Universidade Nova de Lisboa para a obtenção do Grau de Mestre em Engenharia Informática

Conservation GIS: Ontology and spatial reasoning for commonsense knowledge.

Dissertation submitted in partial fulfilment of the requirements for the Degree of Master of Science in Geospatial Technologies.