Monthly Archives: January 2016

A Note on “Disjunctive” Predicates

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

Posted in Uncategorized | Leave a comment


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

Posted in Uncategorized | 2 Comments

Observation Propagation for Importance Sampling with Likelihood Weighting

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

Posted in Uncategorized | Leave a comment

Semantics Challenge

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.
Read the rest
Posted in Uncategorized | 2 Comments