17 citations · 45 across the 13 of their papers we have counts for
15 papers
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…
Preprocessing Source Code Comments for Linguistic Models
Sergey Matskevich, Colin S. Gordon
Comments are an important part of the source code and are a primary source of documentation. This has driven interest in using large bodies of comments to train or evaluate tools t…
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…
Towards Property-Based Tests in Natural Language
Colin S. Gordon
We consider a new approach to generate tests from natural language. Rather than relying on machine learning or templated extraction from structured comments, we propose to apply cl…
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…
Safe Deferred Memory Reclamation with Types
Ismail Kuru, Colin S. Gordon
Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide w…
Synthesizing Program-Specific Static Analyses
Colin S. Gordon
Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of the program analysis, and significant…
Generating Comments From Source Code with CCGs
Sergey Matskevich, Colin S. Gordon
Good comments help developers understand software faster and provide better maintenance. However, comments are often missing, generally inaccurate, or out of date. Many of these pr…
Polymorphic Iterable Sequential Effect Systems
Colin S. Gordon
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect…
A Generic Approach to Flow-Sensitive Polymorphic Effects (Extended Version)
Colin S. Gordon
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect…
Type Inference for Static Compilation of JavaScript (Extended Version)
Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin +4
We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The ty…
Trace Typing: An Approach for Evaluating Retrofitted Type Systems (Extended Version)
Esben Andreasen, Colin S. Gordon, Satish Chandra +3
Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity,…