Semantic foundations of potential-synthesis for expected amortised-cost analysis
We describe ongoing work developing a semantic infrastructure for designing automated and interactive amortised cost analyses based on synthesising potential functions for randomised data structures. These analyses can synthesise amortised complexity bounds that are tight and correct by construction. The architecture combines established and recent ideas from program logics for data structure specification, weakest pre-condition quantitative reasoning, semantics of probabilistic programming, and amortised resource analysis synthesis.
Mon 4 SepDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30
|Continuations and Coexponentials|
Vikraman Choudhury University of Glasgow
|Granite: Compositional Functional Logic Programming|
|Semantic foundations of potential-synthesis for expected amortised-cost analysis|