11 citations · 17 across the 5 of their papers we have counts for
10 papers · 1 filter
Effect Systems as Abstract Interpretations
Colin S. Gordon
Many forms of static reasoning about program behaviours are known in the literature, yet formal relationships are studied surprisingly infrequently. While most type systems are wel…
Error Localization for Sequential Effect Systems (Extended Version)
Colin S. Gordon, Chaewon Yun
We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on…
Modal Abstractions for Virtualizing Memory Addresses
Ismail Kuru, Colin S. Gordon
Operating system kernels employ virtual memory subsystems, which use a CPU's memory management units (MMUs) to virtualize the addresses of memory regions Operating systems manipula…
Natural Language Specifications in Proof Assistants
Colin S. Gordon, Sergey Matskevich
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However…
Designing with Static Capabilities and Effects: Use, Mention, and Invariants
Colin S. Gordon
Capabilities (whether object or reference capabilities) are fundamentally tools to restrict effects. Thus static capabilities (object or reference) and effect systems take differen…
Sequential Effect Systems with Control Operators
Colin S. Gordon
Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This e…