Luca kindly invited me to write a guest post in his blog on CALCO 2007: the 2nd Conference on Algebra and Coalgebra in Computer Science. It is hosted by the University of Bergen in the picturesque city of Bergen (a UNESCO world heritage sight).
I am currently sitting in CALCO-jnr, a workshop of CALCO dedicated to young researchers (mainly Ph.D. students). The CALCO-jnr workshop is being attended by some 35 participants and I find the talks quite interesting and for such a workshop, which is usually meant for work-in-progress type of presentations, of reasonably high quality.
I must admit that the more categorical talks go well beyond my knowledge of this field and thus, I just write a few sentences about the few talks that I could (partially) follow.
- Ichiro Hasuo (a bright young researcher from Kyoto University, currently on leave to do a Ph.D. with Bart Jacobs) presented a very interesting talk on the application of Microcosm principle in Concurrency Theory. The Microcosm principle states that there is an analogy between the structure of the outer world and that of its elements (and in particular, that of the inside world of a human being; see this for an application in mathematics). Ichiro (together with Bart Jacobs and Ana Sokolova) take this idea into Computer Science and use it to prove properties such as congruence of behavioral equivalences (specified by the final model of the co-algebra under consideration) and commutativity and associativity of the operators under consideration. If I understand it correctly, they define a natural transformation that maps the composition operator at the level of co-algebras (e.g., LTSs) to the semantics of the composition of the objects in the carrier of the co-algebra (e.g., sets of pairs of processes indexed with labels). A concrete and tangible application is the way the semantics of parallel composition is defined by the synchronization scheme. Their approach resembles the bi-algebraic approach to operational semantics (e.g., this). A more detailed account of their results is available from here.
- Alexandra Silva presented some thoughts on representing bi-infinite streams, i.e., sequence of the form "... a_{-1} a_{0} a_{1} ..." using other worked-out co-algebraic frameworks for infinite binary trees and infinite streams. I remember a very interesting and accessible talk of Jan Rutten in FMCO 2003 presenting the very interesting co-algebraic treatment of streams which resembles the algebraic analysis techniques we learned in high school. Jan will give a talk on a related topic tomorrow, so you may get to read more about it soon.
- Liam O'Reilly talked about CSP-CASL-Prover which is based on a framework combining CSP as the process language and CASL for algebraic specification (of data types) and thus combines process specification and data specification. Their framework is built upon other tools, namely CSP Prover, which allow for reasoning about CSP processes with CASL data types in Isabelle. Coming from Eindhoven, I wonder whether this type of work can be seen as a rival to mCRL2 toolset and if so, which one will be favored in the long run.
- Francisco Duran talked about the Maude tool environment. He introduced several tools built around Maude, including Interactive Theorem Prover, Termination Tool, and the Real-Time Maude Tool. Interestingly, a number of these tools have a web interface. There is a recent book on Maude, which can be bought from here.
- In the second talk, Dorel Lucanu introduced CIRC which is a tool for proving behavioral equivalences among (possibly infinite) processes specified in Maude.
So much for my first day of CALCO in Bergen; we will be off to a medieval castle for the reception this evening. Stay tuned for the second report!
Greetings from Bergen.
No comments:
Post a Comment