PUReCafe was a weekly scientific colloquium organized by the LMF group.
Moderator: Joost Visser
Attendance open to all.
Upcoming talks
As of September 2006, PUReCafe has been continued with a wider scope as the Theory and Formal Methods Seminar.
Past talks
(reverse chronological)
Thu, 20 July, 2006 at 10:00 
Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications 
João Carlos Silva 
Graphical user interfaces (GUIs) make software easy to use by providing the user with visual controls. Therefore, correctness of GUI's code is essential to the correct execution of the overall software. Models can help in the evaluation of interactive applications by allowing designers to concentrate on its more important aspects. This paper describes our approach to reverse engineer an abstract model of a user interface directly from the GUI's legacy code. We also present results from a case study. These results are encouraging and give evidence that the goal of reverse engineering user interfaces can be met with more work on this technique. 
Thu, 1 June, 2006 at 10:00 
The Quality Economics of DefectDetection Techniques 
Stefan Wagner, Software & Systems Engineering, Technische Universitaet Muenchen, Institut fuer Informatik 
Analytical software quality assurance (SQA) constitutes a significant part of the total development costs of a typical software system. Typical estimates say that up to 50\% of the costs can be attributed to defect detection and removal. Hence, this is a promising area for costoptimisations. The main question in that context is then how to use those different techniques in a costoptimal way. In detail this boils down to the questions to use (1) which techniques, (2) in which order, and (3) with what effort. This talk describes an analytical and stochastic model of the economics of analytical SQA that can be used to analyse and answer these questions. The practical application is shown on the example of a case study on modelbased testing in the automotive domain. 
Thu, 4 May, 2006 at 11:00 
Discussion: Beyond PURe 
Research.PURe team 
The end of the Research.PURe project is approaching. We will be able to look back at a successful project with lots of interesting deliverables. But now it becomes urgent to reflect on what comes after Research.PURe. A deadline for new FCT proposals is July 31. We will initiate discussion about concrete ideas for such a followup project. 
Thu, 23 March, 2006 at 10:00 
Student presentations of course work 
(1) Prototype Implementation of an Algebra of Components in Haskell 
Jácome Cunha 
The starting point to this project are statebased systems modeled as components, i.e, "black boxes" that have "buttons" or "ports" to communicate with the whole system. A list of operators to connect these components is given. A possible way to implement components as coalgebras in Haskell is shown. Finally, a tool to generate a component from a statebased system definition is implemented. 
Thu, 23 March, 2006 at 10:30 
(2) Camila Revival: VDM++ meets Haskell 
Alexandra Silva 
This communication is a follow up of [1]. We show how to model some of the key concepts of VDM++ in Haskell. Classes, objects, operations and inheritance are encoded based on the recently developed OOHaskell library.
[1] Camila Revival: VDM meets Haskell, Joost Visser, J.N. Oliveira, L.S. Barbosa, J.F. Ferreira, and A. Mendes. Overture Workshop, colocated with Formal Methods 2005. 
Thu, 16 March, 2006 at 10:00 
A calculational account of lambdacoinduction 
Alexandra Silva 
This communication is an attempt to apply the calculational style underlying the socalled BirdMeertens formalism to generalised coinduction, as defined in F. Bartels' thesis. In particular, equational properties of such generic recursion scheme are given, relying on its universal characterisation. We also show how corresponding calculational kits for particular instances of the general coinduction are derived by specialisation. 
Thu, 9 March, 2006 at 10:00 
A Local Graphrewriting System for Deciding Equality in Sumproduct Theories 
José Bacelar Almeida 
We present a local graphrewriting system capable of deciding equality on a fragment of the language of pointfree expressions. The fragment under consideration is quite limited since it does not includes exponentials. Nevertheless, it constitutes a nontrivial exercise due to interactions between additive and multiplicative laws. 
Tue, 24 January, 2006 at 11:00 
The essence of dataflow programming 
Tarmo Uustalu, Inst. of Cybernetics, Tallinn 
We propose a novel, comonadic approach to dataflow (streambased) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure contextdependent computation. In particular, we develop a generic comonadic interpreter of languages for contextdependent computation and instantiate it for streambased computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and contextdependent computation. We apply the latter to analyse clocked dataflow (partial streams based) computation. 
Joint work with Varmo Vene, University of Tartu. Appeared in Proc of APLAS 2005. 
Mon, 19 December, 2005 at 14:30 
Strong Types for Relational Databases 
Alexandra Silva 
We define a stronglytyped model of relational databases and operations on them. In this model, table metadata is represented by typelevel entities that guard the semantic correctness of all database operations at compile time. The model relies on typeclass bounded and parametric polymorphism and we demonstrate its encoding in the functional programming language Haskell. Apart from the standard relational database operations, such as selection and joins, we formalize functional dependencies and normalization. We show how functional dependency information can be represented at the type level, and can be transported through operations from argument types to result types. The model can be used for static query checking, but also as the basis for a formal, calculational approach to database design, programming, and migration. The model is available as sublibrary of the UMinho Haskell Libraries, and goes under the name of CoddFish. 
Wed, 30 November, 2005 at 12:30 
Circularization of Strict Multiple Traversal Programs 
João Paulo Fernandes 
Functional programming provides different programming styles for programmers to write their programs in. The differences are even more explicit under a lazy evaluation model, under which a computation of a value is only triggered upon its need. When facing the challenge of implementing solutions for multiple traversals algorithm problems, the functional programmer often tends to assume himself as the decision maker of all the implementation details: how many traversals to define, in which order to schedule them, which intermediate structures to define and traverse, just to name some. Another subparadigm is available, though. Given the proper will and sufficient practice, multiple traversal algorithms are possible to be implemented as lazy circular programs, where some of the programming work is handed to the lazy machinery.In this talk I will present a calculational rule to convert multiple traversal programs into singlepass circular ones. Feedback is more than expected, it is wanted! 
Tue, 12 July, 2005 at 10:30 
Interactive pointfree proof editing 
Zé Pedro Correia 
A BIC was recently assigned to Zé Pedro Correia. Its subject is to develop a tool to manipulate pointfree expressions, according to transformation laws, in order to construct a pointfree proof. This talk will serve to introduce this project to the Research.PURe group, presenting the work done so far and the work to do. We also expect to collect some opinions on the general expected "behaviour" of the tool. 
Tue, 12 July, 2005 at 11:30 
Calculating Circular Programs 
Joao Fernandes 
Abstract to be announced 
Tue, 28 June, 2005 
Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion 
Paulo Silva 
We constructed a tool, called VooDooM, which converts datatypes in VDMSL 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. 
Tue, March 22, 2005 
Transformações Pointwise  Pointfree 
JoseProenca 
Na programação funcional existem vários estilos de programação, não havendo consenso quanto a qual será o melhor. Dois estilos opostos são, por exemplo, pointfree e pointwise, que se distinguem principalmente por no primeiro serem utilizadas variáveis e no segundo não. No trabalho foi introduzida uma possível descrição de expressões em pointfree e em pointwise, de tal forma que estas fossem o mais simples possível. Depois foi introduzido um processo que permite converter expressões entre estes dois tipos. Foram também consideradas outras linguagens pointwise que podem ser convertidas para o tipo pointwise originalmente criado. O principal objectivo foi tornar possível a transição de código pointwise para pointfree, utilizando bases teóricas e com a garantia de que não sejam introduzidos erros no processo de conversão. 
Tue, March 15, 2005 
PURe CAMILA: A System for Software Development using Formal Methods 
João F. Ferreira 
This work consists in the first steps for the reimplementation of CAMILA, which is a software development environment intended to promote the use of formal methods in industrial software environments. The new CAMILA, also called Research.PURe CAMILA, is written in Haskell and makes use of monadic programming. A small prototype interpreter was created, but the purpose of this work is to study the concepts behind such a tool, such as datatype invariants and partial functions. 
Tue, March 8, 2005 
Towards a Catalog of AspectOriented Refactorings 
Miguel Monteiro 
In this paper, we present a collection of aspectoriented refactorings covering both the extraction of aspects from objectoriented legacy code and the subsequent tidying up of the resulting aspects. In some cases, this tidying up entails the replacement of the original implementation with a different, centralized design, made possible by modularization. The collection of refactorings includes the extraction of common code in various aspects into abstract superaspects. We review the traditional objectoriented code smells in the light of aspectorientation and propose some new smells for the detection of crosscutting concerns. In addition, we propose a new code smell that is specific to aspects. 
Tue, February 1, 2005 
Visual Language for Pointfree Programming 
José Miguel Vilaça 
Miguel Vilaça will introduce the topic of designing a visual language for pointfree programming. After this, we will exchange ideas about how to approach this problem. 
Tue, January 18, 2005 
Functional dependency theory made 'simpler' (pdf) 
In the context of Joost Visser's Spreadsheets under Scrutiny talk, I have been looking at refinement laws for spreadsheet normalization. Back to goodold `functional dependency theory', D. Maier's book etc, I ended up by rephrasing of the standard theory using the binary relation pointfree calculus. It turns out that the theory becomes simpler and more general, thanks to the calculus of 'simplicity' and coreflexivity. This research also shows the effectiveness of the binary relation calculus in «explaining» and reasoning about the nary relation calculus «à la Codd». 
JoseNunoOliveira 
Tue, December 21, 2004 
Extreme Grammaring (presentation slides) 
TiagoAlves 
Grammars are to parser generators what programming languages are to compilers. Although parsing is a subset of a well studied area like compilers, grammars were always looked upon as "the ugly duckling". In this presentation I will propose a methodology for developing grammars using the SDF (Syntax Definition Formalism) inspired in Extreme Programming. This methodology was used to develop a grammar for ISO VDMSL, one of the most common languages used for formal specification. The grammar is available from: VooDooMFront. 
Tue, December 14, 2004 
title to be completed 
Damijan Rebernak 
Damijan Rebernak from Maribor University, Slovenia, will present a talk on grammarbased tools. NOTE: The talk will start at 12:00, instead of the usual hour of 11:00. 
Tue, December 7, 2004 
Generalizing the Hyloshift law 
JorgeSousaPinto 
In the Pure Workhsop last Sptember a limitation of the Hyloshift law for program calculation was identified, and a possible way of solving it was then discussed. In this talk I will present my current understanding of how a generalized version of the law can be formalized. 
Thu, Oct 26, 2004 
Spreadsheets under Scrutiny 
JoostVisser 
In this talk we will show how Haskell can be used to process spreadsheets. We will demonstrate a prototype that takes an excell workbook as input, converts it to gnumeric's xml representation of spreadsheets with formulas, reads and parses the xml representation into a strongly type set of haskell datatypes, and finally computes and visualizes the spreadsheet data flow graph. The audience will be invited to suggest interesting spreadsheet analyses and transformations that might be implemented with this infrastructure. 
Thu, 22 July, 2004 
Generalised LR Parsing in Haskell 
Joao Fernandes 
This is a sneak preview of the student presentation João will give at the Summer School on Advanced Functional Programming (Tartu, 21 august, 2004). GLR parsing is a generalization of LR parsing where ambiguous grammars do not lead to parse errors, but to several parsers working in parallel. We have implemented GLR in Haskell relying on lazy evaluation and incremental computation to improve its performance and approach closer to the original imperative formulation of the algorithm. 
Thu, 3 June, 2004 
Data Model Reverse Engineering from Legacy Source Code 
JoostVisser 
The data models of most legacy software systems are not explicitly defined. Instead, they are encoded in the program source code. Using a mixture of program understanding techniques it is possible to (partly) reconstruct these models. In this talk we provide details of a reverse engineering project carried out at the Software Improvement Group. In this project, the software portfolio of a large multinational bank, consisting of many million lines of Cobol code, was analyzed. Both hierarchical databases (IMS) and relational ones (DB2) are used in this portfolio. We will survey the program understanding techniques used, and detail the particular challenges posed by the size and heterogeneity of the analyzed portfolio. 
Thu, 20 may, 2004 
Constrained datatypes and datatype invariants: a relational approach (slides) 
JoseNunoOliveira 
Datatype invariants are a significant part of the business logic which is at the heart of any commercial software application. However, invariants are hard to maintain consistent and their formal verification requires costly «invent and verify» procedures, most often neglected throughout the development lifecycle. We sketch a basis for a calculational approach to maintaining invariants based on a «correct by construction» development principle. We propose that invariants take the place of datatypes in the diagrams that describe computations and use weakest liberal preconditions to type the arrows in such diagrams. All our reasoning is carried out in the relational calculus structured by Galois connections. 
Thu, 6 may, 2004 
Incremental and Lazy Generalised LR Parsing 
JoaoSaraiva 
Parser combinators elegantly and concisely model generalised LL parsers in a purely functional language. They nicely illustrate the concepts of higherorder functions, polymorphic functions and lazy evaluation. Indeed, parser combinators are often presented as "the" motivating example for functional programming. Generalised LL, however, has an important drawback: it does not handle (direct nor indirect) left recursive contextfree grammars. In a different context, the (nonfunctional) parsing community has been doing a considerable amount of work on generalised LR parsing. Such parsers handle virtually any contextfree grammar. Surprisingly, no work has been done on generalised LR by the functional prog. community. In this talk, I will present a concise (100 lines!), elegant and efficient implementation of an incremental generalised LR parser generator/interpreter in Haskell. Such parsers rely heavily on lazy evaluation. Incremental evaluation is obtained via function memoisation. I will present the HaGlr tool: a prototype implementation of our generalised LR parser generator. The profiling of some (toy) examples will be discussed. 
Thu, 1 apr, 2004 
Connectors as relations 
MarcoAntonioBarbosa 
The basic motivation of component based development is to replace conventional programming by the composition and configuration of reusable offtheshelf units externally coordinated, through a network of connecting devices, to achieve a common goal. This work introduces a new relational model for connectors of software components. The proposed model adopts a coordination point of view in order to deal with components temporal and spatial decoupling and, therefore, to provide support for looser levels of intercomponent dependency and effective external control. 
Thu, 25 mar, 2004 
A Unified Approach for the Integration of Distributed Heterogeneous Software Components 
Barrett Bryant 
A framework is proposed for assembling software systems from distributed heterogeneous components. For the successful deployment of such a software system, it is necessary that its realization not only meets the functional requirements but also nonfunctional requirements such as Quality of Service (QoS) criteria. The approach described is based on the notions of a metacomponent model called the Unified Meta Model (UMM), a generative domain model, and specification of appropriate QoS parameters. A formal specification based on TwoLevel Grammar is used to represent these notions in a tightly integrated way so that QoS becomes a part of the generative domain model. A simple case study is described in the context of this framework. 
Thu, 18 mar, 2004 
Gilles Barthe 
Type Isomorphisms and Proof Reuse in Dependent Type Theory 
Thu, 11 mar, 2004 
Generic Sorting by Insertion 
JorgeSousaPinto 
We show that three popular functional sorting algorithms can be seen as having a common structure derived from insertion sort. Slides available here. 
Thu, 4 mar, 2004 
Developing Haskell Software 
Joost Visser 
In this talk, I will give a brief overview of Haskell software development around the world and I will present a lightweight infrastructure to support such development by us. Among other things, I will talk about development tools such as Haddock, QuickCheck, HUnit, and GHood. I will point out some nice development projects that seem relevant to the Research.PURe project, such as the refactoring project in Kent. 
Thu, 26 feb, 2004 
Advanced Functional Programming Project Presentations 
Students 
The students in the course on Advanced Functional Programming will present their project work: Football Robots in HASKELL
 Software Evaluation as a Web service
 Querying and Transforming XML in HASKELL

Thu, 19 feb, 2004 
Pointfree Program Transformation 
AlcinoCunha, JorgeSousaPinto 
Functional programs are particularly well suited to formal manipulation by equational reasoning. In this setting, it is straightforward to use calculational methods for program transformation. Wellknown 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 pointfree 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 higherorder folds calculated systematically from a specification. The machinery of the calculus is expanded with higherorder pointfree 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. 
Thu, 12 feb, 2004 
Transposing Relations: from Maybefunctions to HashTables 
JoseNunoOliveira 
Functional transposition is a technique for converting relations into functions aimed at developing the relational algebra via the algebra of functions. This talk attempts to develop a basis for generic transposition. Two wellknown instances of the construction are considered, one applicable to any relation and the other applicable to simple relations only. Our illustration of the usefulness of the generic transpose takes advantage of the free theorem of a polymorphic function. We show how to derive laws of relational combinators as free theorems of their transposes. Finally, we relate the topic of functional transposition with the hashtable technique for data representation. 
Thu, 29 jan, 2004 
Invitation to Wiki 
AlcinoCunha, JoostVisser 
We will explain the basics of collaborative web editing with Wiki. We will discuss the way we have organized our local Wiki and invite you to contribute to it. Finally we will exchange ideas about how to use the Wiki for our research and education. 


Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

