Software

CAO language

Repository URL: 
http://hackage.haskell.org/package/cao

The CAO language is aimed at writing cryptographic software in a higher abstraction level which is then transformed and compiled to the C language, while preserving the overall safety properties.

The CAO compiler is publicly available from the Hackage repository.

Galculator

The Galculator is a prototype of a proof assistant 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.

It is written in the Haskell programming language resorting to many language extensions, specially GADTs (Generalized Algebraic Data Types).

VooDooM

VooDooM transforms VDM-SL datatype specifications to obtain an equivalent relational representation. This relational representation can be exported as VDM-SL datatypes or translated to SQL table definitions.