Haskell

Showing results in 'Publications'. Show all posts
Silva P, Oliveira JN.  2008.  'Galculator': functional prototype of a Galois-connection based proof assistant. Proceedings of 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. :44-55. Abstractppdp08.pdf

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.
Alves T, Silva P, Visser J.  2012.  Constraint-aware Schema Transformation. Electronic Notes in Theoretical Computer Science. 290:3-18. Abstractrule08.pdf

Data schema transformations occur in the context of software evolution, refactoring, and cross-paradigm data mappings. When constraints exist on the initial schema, these need to be transformed into constraints on the target schema. Moreover, when high-level data types are refined to lower level structures, additional target schema constraints must be introduced to balance the loss of structure and preserve semantics.

We introduce an algebraic approach to schema transformation that is constraint-aware in the sense that constraints are preserved from source to target schemas and that new constraints are introduced where needed. Our approach is based on refinement theory and point-free program transformation. Data refinements are modeled as rewrite rules on types that carry point-free predicates as constraints. At each rewrite step, the predicate on the reduct is computed from the predicate on the redex. An additional rewrite system on point-free functions is used to normalize the predicates that are built up along rewrite chains.

We implemented our rewrite systems in a type-safe way in the functional programming language Haskell. We demonstrate their application to constraint-aware hierarchical-relational mappings.
Silva P, Oliveira JN.  2008.  Report on the Design of a Galculator. Abstracttechicalreport-fast-08-01.pdf

This report presents the Galculator, a tool aimed at deriving equational proofs in arbitrary domains using Galois connections as the fundamental concept. When combined with the pointfree transform and the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification.

We show how rewriting rules derived from the properties of the Galois connections are applied in proofs using a strategic term rewriting system which, in the current prototype, is implemented in Haskell. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed.
Silva P.  2009.  On the Design of a Galculator. Abstractthesis.pdf

The increased complexity of software systems together with the lack of tools and technique to support their development led to the so-called "software crisis". Different views about the problem originated diverse approaches to a possible solution, although it is now generally accepted that a "silver bullet" does not exist.
The formal methods view considers mathematical reasoning as fundamental to fulfill the most important property of software systems: correctness. However, since correctness proofs are generally difficult and expensive, only critical applications are regarded as potential targets for their use. Developments in tool support such as proof assistants, model checkers and abstract interpreters allows for reducing this cost and making proofs affordable to a wider range of applications. Nevertheless, the effectiveness of a tool is highly dependent of the underlying theory.
This dissertation follows a calculational proof style in which equality plays the fundamental role. Instead of the traditional logical approach, fork algebras, an extension of relation algebras, are used. In this setting, Galois connections are important because they reinforce the calculational nature of the algebraic approach, bringing additional structure to the calculus. Moreover, Galois connections enjoy several valuable proper- ties and allow for transformation in the domain of problems. In this dissertation, it is shown how fork algebras and Galois connections can be integrated together with the indirect equality principle. This combination offers a very powerful, generic device to tackle the complexity of proofs in program verification. This power is enhanced with the design of an innovative proof assistant prototype, the Galculator.