[PRL] POPL Trip Report (part 2 of 2)

[Mitchell Wand]

Alas, I have to leave tonite, so this will be the last installment.  Enjoy.
--Mitch
================================================================

Invited Talk: Walter Fontana, Systems Biology, Harvard Medical School
Systems Biology & Programming Languages

This guy is a molecular biologist with a more-than-passing interest in
CS and PL in particular. (He's found the shortest term for predecessor
on Church numerals, using a genetic algorithm!).

He's been working with Vincent Danos and several other heavyweights.
Danos has a language called Kappa for describing molecular
interactions.  The speaker claims that this language is good for
describing models and suggesting the questions that wetlab biologists
should ask.  (NOT in themselves as answering biological
questions). "Models as a communication medium".

eg if you do analysis of a Kappa program (AKA a model of a biological
system), you can find possible pathways, etc.

He also has a startup in Cambridge, called Plectix BioSystems,
producing "Kappa Factory: a model-based reasoning environment useful
to every molecular biologist".  (They do NOT have a website, but write
to andrea at plectix.com for employment opportunities.  They are looking
for a senior technologist + others).

In any case we should invite him to give a talk (Distinguished
Lecture?)

================================================================

Mechanizing Metatheory -- talk from one of the Penn guys.

He talked about the locally-nameless representation they favor.  This
was all stuff I'd heard about before.

Question:  would BUBS be useful in this context?  Would the
locally-nameless representation be useful for BUBS?

================================================================

Iulian Niamtiu
Context Effects for Dynamic Software Updating

This is a student of Michael Hicks at MD.  He presented a
type-and-effect system that takes into account effects both before and
after the current statement.  They've built a tool applying this to C.
An interesting blend of theory and practice.  I spoke to him in the
afternoon, and he emphasized his pragmatic motivations.  He might fit
nicely in the space between PL and Systems.

================================================================

Katherine Moore
High-Level Small-Step Operational Semantics for Transactional Memory

Subject says it all.  I was disappointed, but I might have been too
harsh.

================================================================


Martin Abadi
Semantics of Transactional Memory and Automatic Mutual Exclusion

Martin presented a model called Automatic Mutual Exclusion (AME).  In
this model, transactions are the default, not the exception.  As a
result, the programmer needs to worry about only a few interleavings.
I think the tradeoff is that programmers need to write their threads
cooperatively, by calling yield sufficiently often.  But I'm not sure
of this.

The semantics seems very clean.  He says there are proofs of
correctness of several implementation strategies, but I haven't looked
at the paper yet.

His co-authors on this include Tim Harris, who's done a bunch in STM,
and Andrew Birrell, who is an old-time systems guy who designed some
of the early RPC protocols.  My systems reading list includes several
of his papers from the 80's.

We should definitely have this presented in pl-seminar, possibly near
Katherine Moore's paper.

================================================================
-------------- next part --------------
HTML attachment scrubbed and removed