The Monitor Calculus: Modular Metatheories for Contract Systems
- 講者游書泓 博士 (美國西北大學)
邀請人：陳亮廷 - 時間2025-08-22 (Fri.) 10:00 ~ 12:00
- 地點資訊所新館106演講廳
摘要
Modern contract systems equip programmers with a lightweight tool for specifying and enforcing correct behavior of programs through higher-order run-time assertions.
After two decades, researchers have built a solid theoretical foundation that covers every little detail of the design of contract systems, from the design of expressive notations for contracts, to the correct enforcement of contracts for higher-order functions, and even to the correct asymptotic behavior of optimized contract systems.
Although each paper contributes important new insights, researchers have to define a separate contract calculus for the purpose of establishing domain-specific properties of interest.
As a result, the literature contains a large number of similar but subtly different contract calculi. While each calculus is augmented with domain-specific information, most contract calculi share a common basis.
Consequently, proving each calculus correct and establishing the desired domain-specific properties require a considerable amount of repeated labor.
I address the problem in two steps. First, I introduce the monitor calculus, a parameterized calculus that abstracts over the common parts of various higher-order contract systems in the literature.
Second, building on the monitor calculus, I develop a novel transition-system-based theory that enables the reuse of definitions and metatheories for contract systems.
In this talk, I will present the monitor calculus and demonstrate how it eliminates boilerplate in the proofs by applying the monitor calculus to prove both the correctness space-efficient contracts and its asymptotic time complexity.
After two decades, researchers have built a solid theoretical foundation that covers every little detail of the design of contract systems, from the design of expressive notations for contracts, to the correct enforcement of contracts for higher-order functions, and even to the correct asymptotic behavior of optimized contract systems.
Although each paper contributes important new insights, researchers have to define a separate contract calculus for the purpose of establishing domain-specific properties of interest.
As a result, the literature contains a large number of similar but subtly different contract calculi. While each calculus is augmented with domain-specific information, most contract calculi share a common basis.
Consequently, proving each calculus correct and establishing the desired domain-specific properties require a considerable amount of repeated labor.
I address the problem in two steps. First, I introduce the monitor calculus, a parameterized calculus that abstracts over the common parts of various higher-order contract systems in the literature.
Second, building on the monitor calculus, I develop a novel transition-system-based theory that enables the reuse of definitions and metatheories for contract systems.
In this talk, I will present the monitor calculus and demonstrate how it eliminates boilerplate in the proofs by applying the monitor calculus to prove both the correctness space-efficient contracts and its asymptotic time complexity.