Search

A área financeira é conhecida por ter processos complexos, que necessitam de envolvência humana, com tempos de esperar longos e que recorrem a entidades externas nos processos de verificação e validação, aumentando os custos associados com as transações. Para tal o desenvolvimento tecnológico é um elemento chave no desenvolvimento da área, na mitigação destes problemas e na criação de novos sistemas que permitam diminuir custos para as entidades financeiras e melhorar o serviço ao utilizador final. O aparecimento da tecnologia Blockchain veio permitir a criação de sistemas que eliminam todos os problemas indicados, automatizando os processos e eliminando a mão humana, criando confiança no sistema de maneira a eliminar o recurso a entidades externas e desta forma diminuindo o tempo de espera e os elevados custos de intermediação. O objetivo desta dissertação é exatamente procurar se a área financeira tem a intencionalidade de aplicar a tecnologia Blockchain nos seus sistemas, de maneira a diminuir os elevados custos e oferecer um melhor serviço aos seus clientes. Para tal, foi feita um investigação qualitativa, com recurso a entrevistas semiestruturadas a profissionais da área financeira, foi também realizada uma pesquisa bibliográfica detalhada sobre a tecnologia Blockchain no sentido de apurar quais as características que a mesma possui que proporcionam os benefícios indicados, os riscos associados à sua aplicação e quais os projetos já existentes sobre esta temática, fazendo depois a ligação à realidade portuguesa através das respostas obtidas nas entrevistas realizadas. The financial area is known for having complex processes, which requires human involvement, with long waiting times and resorting to external entities in the verification and validation processes, increasing the costs associated with transactions. Technological development is a key element in the development of the financial area, in the mitigation of these problems and creation of new systems that allow reducing costs for financial institutions and improving the service to the end user. The emergence of Blockchain technology has allowed the creation of systems that eliminate all the indicated problems, automating the processes and eliminating the human hand, creating trust in the system in order to eliminate the use of external entities and thus reducing the waiting time and the high intermediation costs. The objective of this dissertation is precisely to find out if the financial area intends to apply Blockchain technology in its systems, in order to reduce the high costs and offer a better service to its customers. To this end, a qualitative investigation was carried out, using semi-structured interviews with professionals in the financial area, a detailed bibliographic research was also carried out on Blockchain technology in order to determine which characteristics it has that provide the indicated benefits, risks associated with its application and which projects already exist on this theme, making the connection to the Portuguese reality through the answers obtained in the carried out interviews.

This paper introduces the metaphorism pattern of relational specification and addresses how specification following this pattern can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement proposed in this paper is a strategy known as change of virtual data structure. It gives sufficient conditions for such implementations to be calculated using relation algebra and illustrates the strategy with the derivation of quicksort as example., The author wishes to thank the anonymous referees for their comments and suggestions. This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Funda¸c˜ao para a Ciˆencia e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020537

Techn. Report TR-HASLab:01:2013, The production of safety critical software is bound to a number of safety and certification standards in which estimating the risk of failure plays a central role. Yet risk estimation seems to live outside most programmers’ core practice, involving simulation techniques and worst case analysis performed a posteriori. In this paper we propose that risk be constructively handled in functional programming by writing programs which choose between expected and faulty be- haviour and by reasoning about them in a linear algebra extension to the standard algebra of programming. In particular, the paper calculates propagation of faults across standard program transformation techniques known as tupling and fusion, enabling the fault of the whole to be expressed in terms of the faults of its parts., Fundação para a Ciência e a Tecnologia (FCT)

Non-trivial bidirectional transformations (BXs) are inherently ambiguous, as there are in general many different ways to consistently translate an update from one side to the other. Existing BX languages and frameworks typically satisfy fundamental first principles which ensure acceptable and stable (well-behaved) translation. Unfortunately, these give little insight about how a particular update translation is chosen among the myriad possible. From the user perspective, such unpredictability may hinder the adoption of BX frameworks. The problem can be remedied by imposing a “principle of least change” which, in a state-based framework, amounts to translating each update in a way such that its result is as close as possible to the original state, according to some distance measure. Starting by formalizing such BXs focusing on the particular framework of lenses, this paper discusses whether such least-change lenses can be defined by composition, an essential construct of BX frameworks. For sequential composition, two (dual) update translation alternatives are presented: a classical deterministic one and a nondeterministic. A key ingredient of the approach is the elegant formalization of the main concepts in relation algebra, which exposes several similarities and dualities., Electronic Communications of the EASST, Volume 57: Bidirectional Transformations 2013

Inspired by the trend on unifying theories of programming, this paper shows how the algebraic treatment of standard data dependency theory equips relational data with functional types and an associated type system which is useful for type checking database operations and for query optimization. Such a typed approach to database programming is then shown to be of the same family as other programming logics such as eg. Hoare logic or that of strongest invariant functions which has been used in the analysis of while statements. The prospect of using automated deduction systems such as Prover9 for type-checking and query optimization on top of such an algebraic approach is considered., Fundação para a Ciência e a Tecnologia (FCT)

There is a need for a language able to reconcile the recent upsurge of interest in quantitative methods in the software sciences with logic and set theory that have been used for so many years in capturing the qualitative aspects of the same body of knowledge. Such a lingua franca should be typed, polymorphic, diagrammatic, calculational and easy to blend with traditional notation. This paper puts forward typed linear algebra (LA) as a candidate notation for such a role. Typed LA emerges from regarding matrices as morphisms of suitable categories whereby traditional linear algebra is equipped with a type system. In this paper we show typed LA at work in describing weighted (prob- abilistic) automata. Some attention is paid to the interface between the index-free language of matrix combinators and the corresponding index- wise notation, so as to blend with traditional set theoretic notation., Fundação para a Ciência e a Tecnologia (FCT)

There is a need for a language able to reconcile the recent upsurge of interest in quantitative methods in the software sciences with logic and set theory that have been used for so many years in capturing the qualitative aspects of the same body of knowledge. Such a lingua franca should be typed, polymorphic, diagrammatic, calculational and easy to blend with traditional notation. This paper puts forward typed linear algebra (LA) as a candidate notation for such a role. Typed LA emerges from regarding matrices as morphisms of suitable categories whereby traditional linear algebra is equipped with a type system. In this paper we show typed LA at work in describing weighted (prob- abilistic) automata. Some attention is paid to the interface between the index-free language of matrix combinators and the corresponding index- wise notation, so as to blend with traditional set theoretic notation.

Available for individual study only., Although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education. In particular, logic, which is central to algorithm development, is rarely taught explicitly at preuniversity level, under the justification that it is implicit in mathematics and therefore does not need to be taught as an independent topic. This paper argues in the opposite direction, describing a one-week workshop done at the University of Minho, in Portugal, whose goal was to introduce to high-school students calculational principles and techniques of algorithmic problem solving supported by calculational logic. The workshop resorted to recreational problems to convey the principles and to software tools, the Alloy Analyzer and Netlogo, to animate models., On- going collaboration with Roland Backhouse is deeply acknowledged. This research was supported by the MathIS project under contract PTDC/ EIA/ 73252/ 2006. The first two authors were further supported by FCT grants SFRH/ BD/ 24269/ 2005 and SFRH/ BD/ 29553/ 2006, respectively.

"Technical Report No. TR-IIS-10-009", Problem statements often resort to superlatives such as in eg. “. . . the smallest such number”, “. . . the best approximation”, “. . . the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part). This paper introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution being sought. The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.

Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrix multiplication, the kernel operation of matrix algebra, ranging from its divide-and-conquer version to the conventional, iterative one. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix com- binators but also found a way of addressing other operations calculation- ally such as e.g. Gaussian elimination. A strategy for addressing vector- ization along the same lines is also given., FCT, Mondrian Project funded by contract PTDC/EIA-CCO/108302/2008.

Relatório de estágio do mestrado em Ensino da Educação Física nos Ensinos Básico e Secundário, apresentado à Fac. de Ciências do Desporto e Educação Física da Universidade de Coimbra O presente relatório tem como objectivo explanar a minha actividade como professor estagiário ao longo do ano lectivo 09/10, no Agrupamento de escolas de Montemor-o-Velho, leccionando a turma do 10º A. Este processo de estágio é o culminar de uma formação realizada e direccionada para o ensino da Educação Física, nas escolas do ensino Básico e Secundário. Neste documento tento, de forma clara e perceptível, demonstrar o meu desempenho em duas dimensões: a actividade ensino-aprendizagem (planeamento/realização/avaliação) e a componente ético-profissional, salientando, por um lado, as dificuldades e os obstáculos, por outro, os sucessos atingidos em contexto real de ensino. Pretende-se igualmente evidenciar as metodologias e estratégias de ensino, bem como os instrumentos utilizados, para desenvolver o processo de ensino-aprendizagem dos alunos, reflectindo e analisando as decisões tomadas no contexto educativo inerente ao processo de estágio.

Galois is a domain specific language supported by the Galculator interactive proof-assistant prototype. Galculator uses an equational approach based on Galois connections with indirect equality as an additional inference rule. Galois allows for the specification of different theories in a point-free style by using fork algebras, an extension of relation algebras with expressive power of first-order logic. The language offers sub-languages to derive proof rules from Galois connections, to express proof tactics, and to organize axioms and theorems into modular definitions. In this paper, we describe how the algebraic theory underlying the proof-method drives the design of the Galois language. We provide the syntax and semantics of important fragments of Galois and show how they are hierarchically combined into a complete language., Theauthorsthanktheanonymousrefereesforinsightfulcomments which improved the quality of the original submission. This research was supported by FCT (the Portuguese Foundation for Science and Technology), in the context of the MATHIS Project under contract PTDC/EIA/73252/2006. The first author was supported by FCT under grant number SFRH/BD/19195/2004.

Tool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel (R) Flash File System Core. We combine high-level manual specification and proofs with current state of the art mechanical verification tools into a tool-chain which involves Alloy, VDM++ and HOL. The use of (pointfree) relation modelling provides the glue which binds these tools together., Mondrian Project funded by the Portuguese NSF under contract PTDC/EIA-CCO/108302/2008

The pointfree transform offers to the predicate calculus what the La- place transform offers to the differential/integral calculus: the possibility of chang- ing the underlying mathematical space so as to enable agile algebraic calculation. This paper addresses the foundations of the transform and its application to a calculational approach to extended static checking (ESC) in the context of ab- stract modeling. In particular, a calculus is given whose rules help in breaking the complexity of the proof obligations involved in static checking arguments. The close connection between such calculus and that of weakest pre-conditions makes it possible to use the latter in ESC proof obligation discharge, where point- free notation is again used, this time to calculate with invariant properties to be maintained. A connection with the “everything is a relation” lemma of Alloy is estab- lished, showing how close to each other the pointfree and Alloy notations are. The main advantage of this connection is that of complementing pen-and-paper pointfree calculations with model checking support wherever validating sizable abstract models., Fundação para a Ciência e a Tecnologia (FCT)

Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Galculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed., (undefined)

Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In par- ticular, it allows for reasoning about confinement in object- oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally., Supported by NNSFC (No. 60573081)

The standard operation refinement ordering is a kind of “meet of op- posites”: non-determinism reduction suggests “smaller” behaviour while increase of definition suggests “larger” behaviour. Groves’ factorization of this ordering into two simpler relations, one per refinement concern, makes it more mathe- matically tractable but is far from fully exploited in the literature. We present a pointfree theory for this factorization which is more agile and calculational than the standard set-theoretic approach. In particular, we show that factorization leads to a simple proof of structural refinement for arbitrary parametric types and ex- ploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed, Fundação para a Ciência e a Tecnologia (FCT) - PURE Project (Program Understanding and Re-engineering: Calculi and Applications), contract POSI/ICHS/44304/2002.

We have experimented with modeling some of the key concepts of the VDM specification language inside the functional programming language Haskell. For instance, VDM’s sets and maps are directly available as data types defined in standard libraries; we merely needed to define some additional functions to make the match complete. A bigger challenge is posed by VDM’s data type invariants, and pre- and post- conditions. For these we resorted to Haskell’s constructor class mechanism, and its support for monads. This allows us to switch between different modes of evaluation (e.g. with or without property checking) by simply coercing user defined functions and operations to different specific types.

We constructed a tool, called VooDooM, which converts datatypes in Vdm-sl into Sql relational data models. The conversion involves transformation of algebraic types to maps and products, and pointer introduction. The conversion is specified as a theory of refinement by calculation. The implementation technology is strategic term rewriting in Haskell, as supported by the Strafunski bundle. Due to these choices of theory and technology, the road from theory to practise is straightforward., Fundação para a Ciência e a Tecnologia (FCT) - POSI/ICHS/44304/2002, Agência de Inovação (ADI) - ∑!2235

This paper suggests functional programming languages with coinductive types as suitable devices for prototyping process calculi. The proposed approach is independent of any particular process calculus and makes explicit the different ingredients present in the design of any such calculi. In particular structural aspects of the underlying behaviour model (e.g. the dichotomies such as active vs reactive, deterministic vs nondeterministic) become clearly separated from the interaction structure which defines the synchronisation discipline. The approach is illustrated by the detailed development in Charity of an interpreter for a family of process languages., (undefined)

A transacted memory that is implemented using EEPROM technology offers persistence, undoability and auditing. The transacted memory system is formally specified in Z, and refined in two steps to a prototype C implementation / SPIN model. Conclusions are offered both on the transacted memory system itself and on the development process involving multiple notations and tools.

In the design of a functional library in the area of data-mining several algorithmic patterns have been identified which call for generic programming. Some of these have to do with flattening functions which arise in a particular group of hierarchical systems. In this paper we describe our efforts to make such functionalities generic. We start by a generic induc- tive construction of the intended class of hierarchical types. We conclude by relating the structure of the relevant base-functors with the algebraic structure which is required by the generic flattening functionality, in particular concerning its “deforestation” towards a linearly complex implementation. The instances we provide as examples include the widely known bill of materials “explode” operation., FCT

Lecture Notes in Computer Science Volume 1349, 1997., This paper accompanies the demonstration of Camila, an experimental platform for formal software development, rooted in the tradition of constructive specification methods. The Camila approach is an attempt to make available at software development level the basic problem solving strategy one got used to from school physics - create, experiment and reason on a mathematical model. Based on a notion of formal software component, it encompasses a set-theoretic language and an inequational calculus for classification and refinement. Its kernel is a functional prototyping environment, fully connectable to external applications, equipped with a classified component repository and distribution facilities., (undefined)