Reasoning About Paths in the Interface Graph

Author Michael Greenberg

Thumbnail PDF


  • Filesize: 0.71 MB
  • 11 pages

Document Identifiers

Author Details

Michael Greenberg
  • Stevens Institute of Technology, Hoboken, NJ, USA


I gratefully acknowledge the reviewers for their advice.

Cite AsGet BibTex

Michael Greenberg. Reasoning About Paths in the Interface Graph. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 11:1-11:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Clearly specified interfaces between software components are invaluable: development proceeds in parallel; implementation details are abstracted away; invariants are enforced; code is reused. But this abstraction comes with a cost: well chosen interfaces let related tasks be grouped together, but a running program interleaves tasks of all kinds. Reasoning about which values cross a given interface or which interfaces a value will cross is challenging. It is particularly hard to know that interfaces apply runtime enforcement mechanisms correctly: as programs run, values cross abstraction boundaries in subtle ways. One particular case of such reasoning - proving that a contract system checks contracts correctly at runtime [Christos Dimoulas et al., 2011; Christos Dimoulas et al., 2012] - uses a dynamic analysis to keep track of which interfaces are responsible for which values. The dynamic analysis works by giving an alternative semantics that "colors" values to match the components responsible for them. No program is ever run in this alternative semantics - it’s a formal tool to verify that the contract system’s enforcement is correct. In this short paper, we refine Dimoulas et al.’s dynamic analysis to more precisely track colors, phrasing our results graph theoretically: a value’s colors are a path in the interface graph of the original program. Our graph theoretic framing makes it easy to see that the dynamic analysis is subsumed by Eelco Visser’s scope graphs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
  • Mathematics of computing → Graph theory
  • Software and its engineering → Abstraction, modeling and modularity
  • interfaces
  • components
  • lambda calculus
  • dynamic analysis


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jack B. Dennis and Earl C. Van Horn. Programming semantics for multiprogrammed computations. CACM, 9(3), March 1966. URL:
  2. Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen. Correct blame for contracts: no more scapegoating. In POPL. ACM, 2011. URL:
  3. Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Complete monitors for behavioral contracts. In ESOP, volume 7211 of LNCS. Springer, 2012. URL:
  4. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In ICFP. ACM, 2002. URL:
  5. Jean-Jacques Lévy. Tracking redexes in the lambda calculus, 2022. In submission. URL:
  6. Mark Samuel Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, Baltimore, Maryland, USA, May 2006. URL:
  7. James H. Morris. Protection in programming languages. CACM, 16(1), January 1973. URL:
  8. Pierre Neron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In ESOP, volume 9032 of LNCS. Springer, 2015. URL:
  9. G.D. Plotkin. Lcf considered as a programming language. Theoretical Computer Science, 5(3):223-255, 1977. URL:
  10. Casper Bach Poulsen, Pierre Néron, Andrew P. Tolmach, and Eelco Visser. Scopes describe frames: A uniform model for memory layout in dynamic semantics. In ECOOP, volume 56 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL:
  11. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. Scopes as types. PACMPL, 2(OOPSLA), October 2018. URL:
  12. Hendrik van Antwerpen, Pierre Neron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In PEPM. ACM, 2016. URL:
  13. Vlad Vergu, Andrew Tolmach, and Eelco Visser. Scopes and Frames Improve Meta-Interpreter Specialization. In ECOOP, volume 134 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL:
  14. Steve Zdancewic, Dan Grossman, and J. Gregory Morrisett. Principals in programming languages: A syntactic proof technique. In ICFP. ACM, 1999. URL: