Seminar at QMUL on CONCUR paper

Tomorrow, Martin will give a seminar at Queen Mary University of London on a recent collaboration with Peter Mosses and Mohammad Reza Mousavi on extending the notion of well-supported proof (for transition systems with negative premises) to open rules. The paper is Modular Semantics for Transition System Specifications with Negative Premises, and it will appear at the CONCUR conference later this year.

Update: slides now available. tonga . web page alert

SLS 2013: Workshop on Scalable Language Specification

In June, PLanCompS will be co-organising a workshop on Scalable Language Specification together with Microsoft Research, Cambridge.

  • Workshop dates: June 25–27, 2013, Cambridge, UK
  • Submission deadline extended: April 2, 2013
  • See the website here

The focus of this workshop is on formal language specification frameworks
and how they scale up when applied to larger languages. The workshop provides
a forum for discussing practical and theoretical issues, and aims to promote
dissemination and collaboration between the developers and users of language
specification frameworks.

There will be 10 Invited speakers: Egon Börger, Mark van den Brand, Kevin Hammond, Sir Tony Hoare, Paul Klint, Shriram Krishnamurthi, José Meseguer,
Grigore Roşu, Dave Schmidt, and Peter Sewell.

Caml Light Grammars

The Caml-light lanugage was released in 1992 by INRIA and the language specification is available from here. The language specification gives a grammar for ‘core’ caml light, split into sections within the specification. Within the html version of the specification, the grammar rules are enclosed within <PRE></PRE> tags and so a simple terminal command such as sed -e ‘/<PRE>/,/PRE>/!d’ $1.* > rules.html can be used to extract the grammar rules for core caml-light.
rulesOrgin is the set of grammar rules extracted from the html files rooted at by the command sed -e ‘/<PRE>/,/PRE>/!d’ $1.* > rules.html.

Unfortunately this set of rules contains some errors: missing nonterminals, repeated terminals and so on.

rulesAfter is a set of grammar rules based on Y, but with errors corrected.

The Caml-light langauge specification lists a set of extension to core caml-light. In practice these extensions are required to parse the majority of Caml-light strings. The extensions are specified as alterations to the existing grammar

rulesEx is a set of grammar rules based on core caml light, but altered by hand to include the extended syntax.

Mohammad Mousavi visit

Today we welcome Mohammad Mousavi who’ll be giving a talk in the Proof, Complexity & Verification seminar at Swansea entitled In Processes, We Believe! On Marrying Process Algebra and Epistemic Logic. Mohammad is visiting for a few days to discuss modular bisimulation theory with the group at Swansea.

Royal Holloway April Meeting

We’ve just got back from a productive meeting in Royal Holloway, discussing the progress of the project so far and next tasks.

  • Adrian and Elizabeth spoke about the toolchain implementation and use of TIF
  • Joe discussed his integration of the tools into the Eclipse environment
  • Rob spoke of abstract syntax tree generation
  • Mark van den Brand discussed GLL parsing for metamodelling
  • Andrew Kennedy described C#, its history and semantics
  • Peter gave a tutorial on Modular SOS
  • Martin spoke of funcon semantics and behavioural equivalence
  • Kathy described her steps towards object-oriented funcons
  • Casper gave a talk on Partial Evaluation.

We look forward to continuing work on the project and collaborations. domain address .

Seminar by Mark van den Brand

Professor Mark van den Brand, who is currently visiting RHUL, will be giving a short seminar on Tuesday 7 February 2012 at the Royal Holloway Campus.  Abstract below.
DSL Design in High Tech Industry
Domain Specific Languages are getting more and more attention.The High Tech Industry has developed towards a very softwareintensive industry. The amount of software to develop and maintain is growing fast, maybe even in some case too fast. This industry is investigating alternative ways to develop their software. Next to outsourcing to suppliers DSLs are also explored. In this talk two topics are addressed. First, ongoing research is presented with respect to the development of a DSL for the generation of a virtual proto in order to reduce testing effort.  In the second part a home-made DSL (SLCO) is presented and the way we formalize the semantics of this DSL. The reason for formalizing the semantics is to be able to proof the correctness of model transformations developed for mapping SLCO to various platforms.

Ken Madlener’s Research Visit

Ken is visiting Swansea for a few months to work with PLanCompS participants on formalisation of bisimulation equations and their robustness under language extensions. Today he will be giving a talk about this. The talk is part of the Proof, Complexity and Verification series at Swansea, and the Mathematical Foundations series at Bath, via a video link. We look forward to hearing all about it!