Weighted programming: a programming paradigm for specifying mathematical models
summary
Defines an imperative language with nondeterministic branching and weighted traces parameterized by a semiring, and gives a denotational semantics via a weakest-precondition calculus and weakest-liberal-precondition variants using least/greatest fixed points for loops. Provides a cheat sheet of semirings (e.g. tropical min-plus semiring for costs, formal languages, naturals for counting), proves WP/WLP on examples: ski rental yields min(n,y) as the cost bound, finds an unfairness bug in a mutual‑exclusion protocol, and derives a Fibonacci identity; all worked as pen‑and‑paper case studies.
AI-written summary · about
chapters (9)
- 0:00Weighted programming vision
- 1:48Ski rental problem example
- 5:00Language syntax and semiring
- 8:59Denotational semantics
- 13:18Loop analysis with invariants
- 16:32Weakest preconditions and non-termination
- 19:26Protocol bug detection
- 20:31Future work challenges
- 22:18Q&A
related talks
49mSemantic Foundations for Probabilistic Programming
30mRelatively Complete Verification of Probabilistic Programs
40mFormal semantics for multi-language programs
19mPanel: Compilation Frameworks
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
15mA Modular Cost Analysis for Probabilistic Programs
29mCertifying Complexity Analysis- 40mFormal semantics for multi-language programs