Program Understanding and Re-engineering: Calculi and Applications




Sep 18 Paper Towards a Coordination Model for Interactive Systems by MarcoAntonioBarbosa, JoseCampos and LuisSoaresBarbosa has been accepted for FMIS'06 (Macau).

July 3 Paper Configurations of Web Services by MarcoAntonioBarbosa and LuisSoaresBarbosa has been accepted for FOCLASA'06 (Bonn, Germany).

July 3 Paper Strong Types for Relational Databases by Alexandra Silva and JoostVisser has been accepted for the Haskell Workshop 2006 (Portland, USA).

June 16 Paper Strongly Typed Rewriting For Coupled Software Transformation (by AlcinoCunha and JoostVisser) accepted by RULE 2006 (Seattle, USA).

May, 26 Paper Transposing Partial Coalgebras (by LuisSoaresBarbosa and JoseNunoOliveira) accepted for publication in TCS, Elsevier.

May, 11 Papers Type-safe two-level data transformation (by AlcinoCunha, JoseNunoOliveira and JoostVisser) and Pointfree factorization of operation refinement (by JoseNunoOliveira and Cesar Rodrigues) have been accepted by FM'06 (Canada).

May, 8 A paper entitled An Orchestrator for Dynamic Interconnection of Software Components, by MarcoAntonioBarbosa and LuisSoaresBarbosa, accepted at MTCoord'06 (Bologna).


Research » PURe » 2LT

Two Level Transformation (2LT)


NOTE: the 2LT project is moving to: 2LT at Google Code.

A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. Examples of two-level data transformations include XML schema evolution coupled with document migration, and data mappings that couple a data format mapping with conversions between mapped formats.

Theory and implementation in Haskell

In the 2LT project we apply theories of calculational data refinement and of point-free program transformation to two-level transformations.


A refinement of an abstract type A into a concrete type B, is witnessed by conversion functions to:A->B (injective and total) and from:B->A (surjective and partial).


Such data refinements can be modeled by a type-changing rewrite system, where each rewite step takes the form A => (B,to,from). In other words, each step produces not only a new type, but also the conversion functions between the old and new type. By repeatedly applying such rewrite steps, complex conversion functions are calculated incrementally while a new type is being derived.


The complex conversion functions derived after type-changing rewriting can be subjected to subsequent simplification using laws of point-free program calculation. The same holds for compositions of conversion functions with queries on the target or source data types. Such simplifications then amount for instance to:

  • generation of efficient low-level data migrations from high-level migrations
  • program migration of queries on the source data type to queries on a target data type

Apart from transformation of point-free functions, we have implemented rewrite systems for transformation of structure-shy functions (XPath expressions and strategic functions), and for transformation of binary relation expressions.


We have implemented both type-changing rewrite systems and type-preserving rewrite systems in Haskell. The implementations involve generalized algebraic datatypes (GADTs), strategy combinators, type-safe representations of types and of functions, and other advanced Haskell techniques.



  • Alcino Cunha, José Nuno Oliveira, Joost Visser. Type-safe Two-level Data Transformation. In Formal Methods 2006, LNCS 4085, pp. 284-299, 2006. © Springer-Verlag. (PDF) A preliminary version with additional material appended appeared as technical report DI-Research.PURe-06.03.01 (see below).

  • Alcino Cunha, Joost Visser. Strongly Typed Rewriting For Coupled Software Transformation. In Proceedings of RULE 2006, ENTCS, to appear. (PDF).

  • Pablo Berdaguer, Alcino Cunha, Hugo Pacheco, Joost Visser. Coupled Schema Transformation and Data Conversion For XML and SQL. In PADL 2007: Practical Aspects of Declarative Languages, to appear. (PDF).

  • Alcino Cunha and Joost Visser, Transformation of Structure-Shy Programs, Applied to XPath Queries and Strategic Functions, In Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2007, to appear. (PDF)

  • Claudia Mónica Necco, José Nuno Oliveira, and Joost Visser, Extended Static Checking By Strategic Rewriting of Pointfree Relational Expressions, Draft of februari 3, 2007. (PDF)


  • Alcino Cunha, José Nuno Oliveira, Joost Visser. Type-safe Two-level Data Transformations -- with derecursivation and dynamic typing, DI-Research.PURe-06.03.01, March 2006. (PDF).


2LT is a sub-library of the UMinho Haskell Libraries. A stand-alone release is also available:


blog stats

r19 - 05 Dec 2007 - 23:40:49 - TiagoAlves
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM