Re: categories and formal verification

[Bas Spitters <spitters@cs.ru.nl>]

We used monads and applicative functors to verify an implementation real=20
integration. We found CT to be convenient in the process:

A computer verified, monadic, functional implementation of the integral.
Russell O'Connor, Bas Spitters
http://arxiv.org/abs/0809.1552
Abstract: We provide a computer verified exact monadic functional=20
implementation of the Riemann integral in type theory. Together with previo=
us=20
work by O=E2=80=99Connor, this may be seen as the beginning of the realizat=
ion of=20
Bishop=E2=80=99s vision to use constructive mathematics as a programming la=
nguage for=20
exact analysis.




Best regards,

Bas

On Tuesday 08 September 2009 09:20:52 David CHEMOUIL wrote:
> Dear colleagues,
>
>
> Some colleagues of mine and myself are currently investigating categorical
> approaches to component-based development for software, in the spirit of =
J.
> L. Fiadeiro's work or of the coalgebra community.
>
> Being new to the discipline, it also implies for them quite some work in
> basic CT itself. Hence, they're looking for some kind of reason making th=
is
> tedious process worth enduring. Elegance of CT is one such reason, Goguen=
's
> or Ehrig's arguments in a few articles are others.
>
> But, although my colleagues, are pretty convinced by the "constructive"
> aspects of CT applied to such matters, they don't see how CT can provide
> support in *verifying* things about systems under study (e.g what does CT
> approaches bring to check the absence of deadlocks in a concurrent
> system?).
>
> I couldn't find convincing examples, even in Goguen's Manifesto, so I
> wondered whether you had good arguments and/or references to such
> convincing work, that would give them the impetus to continue studying th=
is
> topic.
>
> Regards,
>
> dc


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]