The WS-CDL definition, currently a W3C candidate recommendation, describes a language which is meant for characterising interactions between distinct web services. However, so far there are few tools that allow to check and execute specifications written in the new WS-CDL language. Apart from missing tool support, many basic language features are currently poorly understood. In contrast to traditional languages for describing Web Service interaction, the WS-CDL does not describe traditional two-party communications from the point-of-view of one of the participants. Rather, the WS-CDL language describe interaction scenarios involving multiple parties and from a viewpoint independent of its process participants. To allow us to experiment with the new language, and in general gain more insight in the design principles of the WS-CDL standard proposal, we have implemented a tool that allow us to syntax check, execute and debug WS-CDL descriptions, and which in the near future will allow model checking of WS-CDL descriptions.
Generic Haskell is a language extension of Haskell for polytypic programming. Constrained types are parametric algebraic types with at least one argument constrained by type-class membership. We explain Generic Haskell, discuss the relevance of constrained types, and show that they are not supported by Generic Haskell. We propose context-parametric polykinded types as a solution, thereby making polytypic functions generic on a larger class of types. Our proposal entails an extension to the Generic Haskell compiler, not the language, and is therefore transparent to the generic programmer
We describe a project to refine the idea of proof-directed debugging. The intention is to clarify the mechanisms by which failed verification attempts can be used to isolate errors in code, in particular by exploiting the ways in which the branching structure of a proof can match the the structure of the functional program being verified. Our intention is to supply tools to support this process. We then further discuss how the proof planning paradigm might be used to supply additional automated support for this and, in particular ways in which the automation of proof-directed debugging with proof planning would allows code patches to by synthesised at the same time that a bug is located and diagnosed
This file was generated by bibtex2html 1.98.