[PL-sem-jr] Talk tomorrow, Mon 1/25

[Vincent St-Amour]

Mon 1/25 Room TBA 10:00-12:00

Aaron will finish his talk from last week on concurrency, and Dan will
talk about his research, title and abstract below.

Let's meet in 308 and grab one of the first floor's rooms.



Towards typing probabilistic assertions: How to abstract your
λ-calculus to a process algebra

Programming is hard; probabilistic programming is harder. Just as
assertions help debug and verify deterministic programs, we see
probabilistic assertions as an important tool for verifying
probabilistic programs. To this end, we're designing a type-and-effect
system for a probabilistic λ-calculus to compute lower bounds on the
probability that assertions in a program are true—in general this is
quite hard, so we've made some important simplifying assumptions to
help get us started. I will present our notion of probabilistic
assertions and what it means for one to be true; our language,
type-and-effect system, and the proof of soundness we devised; and
close with the remaining problems and some of Aaron's wacky ideas
about how to solve them.