Thursday, April 28, 2016

Summer school on bidirectional transformations

Lady Margaret Hall, Oxford, UK
25th to 29th July 2016


Bidirectional transformations (BX) are means of maintaining consistency between multiple information sources: when one source is edited, the others may need updating to restore consistency. BX have applications in databases, user interface design, model-driven development, and many other domains. This summer school is one of the closing activities on the "Theory of Least Change for BX" project at Oxford and Edinburgh. It brings together leading researchers in BX, spanning theory and
practice, for a week of lectures in beautiful Oxford. It will be aimed at doctoral students in computer science, but will also be suitable for strong master's students and for researchers.

Read more »

Labels: ,

Tuesday, March 01, 2016

PhD studentships in programming languages, provenance, data management

I am currently advertising two PhD studentships, on topics spanning programming languages, provenance, and data management, to start in fall 2016. 

Both of these studentships are fully funded for applicants of any nationality (in contrast to many UK PhD studentships which are only funded up to the UK/EU tuition level, and do not cover full tuition fees for students from outside the European Union.)
Read more »

Labels: , , , , , ,

Wednesday, January 13, 2016

Reflections on monadic lenses

Thanks to Matt Might for some very kind words on our paper "Reflections on monadic lenses", recently posted to and scheduled to appear in April as part of an upcoming Festschrift for Phil Wadler.

Labels: ,

Thursday, November 05, 2015

Private type members in Scala aren't

I haven't posted in a while now, and one major reason is that I've been teaching a new course on Programming Languages.  I've been using Scala, somewhat experimentally, and as a (perhaps misguided) way of forcing myself to learn some Scala.

In the last few lectures, I've been covering Scala's object system.  I'm not an expert on Scala by any means, but I was a little surprised by the way "private" appears to work (or more accurately, not work) on type members of classes/objects.

Read more »

Labels: ,

Friday, July 24, 2015

Call for participation: DBPL 2015

The 15th International Symposium on Database Programming Languages
Pittsburgh, Pennsylvania, USA
October 27, 2015
hosted as part of SPLASH 2015

Call for Participation

DBPL has a long tradition of bringing databases and programming languages together. This year we continue this tradition by co-locating DBPL with SPLASH 2015, and presenting an interesting mix of papers with programming language and database aspects. In addition to these papers we have an excellent invited talk by Marko Rodriguez of DataStax about Gremlin: A Stream-Based Functional Language for OLTP and OLAP Graph Computing. We hope to see you in Pittsburgh!

DBPL is held in cooperation with ACM SIGPLAN, and gratefully acknowledges support from LogicBlox, Inc.

Read more »

Labels: , ,

Tuesday, April 14, 2015

Mechanized formalizations of the pi-calculus (and friends)

I recently started to put together a bibliography (as complete as I can make it) of mechanized formalizations of the pi-calculus (and close relations).  I also asked for additional suggestions on the TYPES mailing list, and received several helpful responses.  Here is the complete list, as of today.

I hope to use this as a starting point to understand the strengths and weaknesses of different approaches (and any gaps in the literature) but so far I have not read most of these papers.  Nevertheless I am posting this without any further discussion in case it is helpful to anyone else interested in this topic in the future.

Thanks to Robert Harper, Dale Miller, Dominic Orchard, Francois Pottier, Ivan Scagnetto, Gabriel Scherer, and Tjark Weber for their suggestions.

[Updated: Thanks also to Tobias Nipkow and Jeremy Siek for spotting some typos and misclassifications, and Alan Schmitt for a link to more information on HOCore.]

[Updated 2: to include Christine Rockl's MERLIN 2001 paper on a formalization of the pi-calculus in Isabelle/HOL using Gabbay-Pitts permutation-based syntax.]

[Updated 3: to include more recent work on formalising psi-calculi using Nominal Isabelle.]
Read more »

Labels: ,

Wednesday, January 14, 2015

How to publish research accompanied by mechanically-checkable proofs

I've both written and reviewed research papers that incorporate mechanically-checked proofs (either as the main subject of the research or as supporting the correctness of other contributions).  Computer-aided formalization and proof are increasingly part of the mainstream of (the formal side of) programming languages research, and seem to be being especially enthusiastically adopted by students and junior researchers.  However, just having mechanically verified a proof of (some aspect of) a system is not enough - all of the standard considerations regarding the reporting of scientific research, on-paper proofs, or research code still apply. 

This post collects some guidelines that I hope will be helpful for researchers working on papers accompanied by formal proofs. I would have thought most of these were obvious, but have encountered enough counterexamples to disabuse me of this naive assumption.  The following is probably not an exhaustive list, but is offered as a starting point.

Read more »

Labels: ,