Contract System Metatheories à la Carte: A Transition-System View of Contracts
summary
Models higher-order contracts as a parameterized transition system and proves that composing annotations and registers yields reusable metatheory: ownership labels recover correct blame assignment, pairing an unoptimized copy of contracts preserves checks to guarantee space-efficiency correctness, and a primitive-operation counter proves that redundant-check elimination removes asymptotic slowdowns. A mechanized development is available mechanized in Agda (linked repo), and the paper shows instance projections induce transition-system homomorphisms that let one reuse prior proofs across instances.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 3:15Parameterized contract calculus
- 5:22Proofs with annotations
- 7:08Transition systems
- 10:45Modular proofs
- 11:28Q&A
related talks
27mC4: verified transactional objects
57mPerspectives on Contracts for C++
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
41mA Modular Compositional Approach to Engineering Complex Systems
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
56mContracts for Dependable C++
01h 17mFunction Contracts in Practice using C++
28mReasoning about Distributed Reconfigurable Systems