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.
This week, Martin and Peter will be at ETAPS, Rome. Martin will be presenting their paper Modular Bisimulation Theory for Computations and Values as part of FoSSaCS, tomorrow at 4pm.
Update: the slides are now available.
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
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.
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 http://caml.inria.fr/pub/docs/manual-caml-light/node3.html 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.
A very warm welcome to our new postdoc, Paolo Torrini [http://www.cs.le.ac.uk/people/pt95/], who joined the Swansea team on 1st October.
Paolo research will focus mainly on component-based semantics, in collaboration with Martin and Peter.
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.
PLanCompS will be represented at the Summer School on Language Frameworks 2012 in Romania. For more details see https://fmse.info.uaic.ro/events/SSLF12/.
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 .
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 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!