During my talk yesterday, somebody raised an important point when I discussed the Hoare rule for non-deterministic choice in the recursive semantics and claimed that the postcondition couldn’t be disjunctive: What if it was the negation of a conjunction?

I think I waved this away with a gesture towards the constructive Coq proof assistant, but that was in error (the Coq real number library actually posits the decidability of the reals).… Read the rest

As per the discussion at the end of the meeting yesterday: If you have open questions you’d like to share, please do so in comments here. If there’s enough interest, perhaps these could be collated into a more formal document.… Read the rest

Thanks to everyone (presenters, participants, POPL organizers, volunteers…) for making today’s workshop such a lively exchange of knowledge and human connections. Please post slides, posters, preprints, questions, comments, suggestions here on our blog.

Maybe it’s worth having a workshop like this again next year.… Read the rest

A universal probabilistic programming language consists of a general-purpose language extended with two probabilistic features: the ability to make random (probabilistic) choices and the ability to make observations. For expressiveness and efficiency, it is useful to consider observations that have nonnegative real likelihoods rather than simple boolean truth values.… Read the rest

We have several papers proposing denotational semantics for various PP formalisms.  It would be good to be able to compare them.  Here’s a challenge to the authors of these papers:

For your semantics, please give a few examples of each of the following:

1. interesting equivalences between open terms that are equated in your semantics.