About Me


I'm a fifth and final year PhD student interested providing strong static guarantees about program behavior, particularly for concurrent and systems-level code. So I study programming languages. I'm part of the programming languages and software engineering (PLSE) group at UW.

I will be on the job market this fall, for academic and industrial research positions. See below.

For my thesis, I'm developing an approach to verifying serial and concurrent programs using fine-grained descriptions of interference and capabilities for heap mutation, attached to every reference in a program. My thesis committee consists of Michael Ernst, Dan Grossman, and Matt Parkinson.

In the past I was an undergrad at Brown University, where I worked with Shriram Krishnamurthi and Maurice Herlihy. I've interned with NetApp's filesystem group, the Solaris kernel group at Sun pre-Oracle, and have been both a full-time employee (before grad school) and intern (during grad school) with a systems incubation group at Microsoft.

News

  • 4/14: The GUI Effect Checker from my JavaUI paper (ECOOP'13) is now part of the Checker Framework.
  • 2/14: I will be on the PC for IWACO 2014, affiliated with ECOOP 2014.
  • 11/13: I have posted my job application packet.
  • 9/26/13: I'm now the proud father of Henry Ryan Gordon!
  • 5/20/13: I will be giving an invited talk at Languages for the Multicore Era (LaME) 2013.
  • 3/4/13: "JavaUI: Effects for Controlling UI Object Access" will appear at ECOOP'13.
  • 2/4/13: "Rely-Guarantee References for Refinement Types over Aliased Mutable Data" will appear at PLDI'13.

Job Market

I am on the job market, looking for academic (tenure-track assistant professor) and industrial research positions.

  • CV: pdf
  • Research Statement: pdf
  • Teaching Statement: pdf
  • Representative publications (abstracts below):
    • OOPSLA'12: Uniqueness and Reference Immutability for Safe Parallelism (pdf)
    • PLDI'13: Rely-Guarantee References for Refinement Types over Aliased Mutable Data (pdf)
    • ECOOP'13: JavaUI: Effects for Controlling UI Object Access (pdf)
  • References:

Publications


Partial publication lists are also available on Google Scholar, the ACM portal, and DBLP.

In Preparation

  • Towards Heaps in Dependent Type Theory.
    Colin S. Gordon.
    [+abstract]
  • Rely-Guarantee References for Lock-Free Data Structures.
    Colin S. Gordon, Michael D. Ernst, Dan Grossman, and Matt Parkinson.
    Submitted November, 2013.
    [+abstract] [code]

Conference Papers

  • JavaUI: Effects for Controlling UI Object Access.
    In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP'13), Montpellier, France. July 2013.
    Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman.
    Acceptance rate 25% (29/116).
    [+abstract] [+bibtex] [ springer | pdf | tech report] [slides] [new code] [old code]
    This project has now been incorporated into the Checker Framework.
  • Rely-Guarantee References for Refinement Types over Aliased Mutable Data.
    In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), Seattle, WA, USA. June 2013.
    Colin S. Gordon, Michael D. Ernst, and Dan Grossman.
    Acceptance rate 17% (46/267).
    [+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report] [slides] [code]
  • Uniqueness and Reference Immutability for Safe Parallelism.
    In Proceedings of the 27th ACM SIGPLAN Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA'12), Tucson, AZ, USA. October 2012.
    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy.
    Acceptance rate 26% (59/228).
    [+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report | tech report @ msr ] [slides]
    [Press: slashdot | reddit | hacker news (most coverage misunderstood the work)]

Workshop Papers

  • Static Lock Capabilities for Deadlock Freedom.
    In Proceedings of the 8th Workshop on Types in Language Design and Implementation (TLDI'12), Philadelphia, PA, USA. January 2012.
    Colin S. Gordon, Michael D. Ernst, and Dan Grossman.
    [+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report] [slides] [conference homepage]
  • Formal Semantics for Testing.
    In Off the Beaten Track Workshop (OBT'12), Philadelphia, PA, USA. January 2012. Position paper.
    Colin S. Gordon.
    [+abstract] [+bibtex] [pdf] [slides] [conference homepage | schedule]
  • Composition with Consistent Updates for Abstract State Machines.
    In Proceedings of the 14th International Workshop on Abstract State Machines (ASM'07), Grimstad, Norway. June 2007.
    Colin Gordon, Leo Meyerovich, Joel Weinberger, and Shriram Krishnamurthi.
    [+abstract] [+bibtex] [pdf] [proceedings]

Theses and Technical Reports

  • JavaUI: Effects for Controlling UI Object Access (Extended Version).
    Technical Report UW-CSE-13-04-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA. April 2013.
    Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman.
    [+abstract] [+bibtex] [ dept pdf | dept TRs] [code]
  • Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (Extended Version).
    Technical Report UW-CSE-13-03-02, Computer Science and Engineering, University of Washington, Seattle, WA, USA. March 2013.
    Colin S. Gordon, Michael D. Ernst, Dan Grossman.
    [+abstract] [+bibtex] [pdf ] [dept pdf | dept TRs]
  • Uniqueness and Reference Immutability for Safe Parallelism (Extended Version).
    Technical Report MSR-TR-2012-79, Microsoft Research, Redmond, WA, USA. August 2012.
    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy.
    [+abstract] [ pdf | pdf @ msr ]
  • Static Lock Capabilities for Deadlock Freedom.
    Technical Report UW-CSE-11-10-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA. October 2011.
    Colin S. Gordon, Michael D. Ernst, Dan Grossman.
    [+abstract] [+bibtex] [pdf ] [dept pdf | dept TRs]
  • Type-Safe Stack Traversal for Garbage Collector Implementation.
    Brown University Senior Honors Thesis. May 2008. Undergraduate Thesis.
    Colin Stebbins Gordon.
    [+abstract] [+bibtex] [pdf] [slides] [other honors theses]
  • ASM Relational Transducer Security Policies.
    Technical Report CS-06-12, Computer Science Department, Brown University, Providence, RI, USA. November, 2006.
    Meyerovich, L.A., Weinberger, J.H.W., Gordon, C.S., Krishnamurthi, S.
    [+abstract] [+bibtex] [pdf ] [department page]
    This report is essentially an extended version of Composition with Consistent Updates for Abstract State Machines

Patents

  • Merging Containers in a Multi-Container System.
    US Patent 7828201. Filed April, 2007, issued November 2010. Assigned to Network Appliance.
    Colin Stebbins Gordon, Pratap Vikram Singh, and Donald Alvin Trimmer.
    [ Patent at USPTO ]
  • Data Containerization for Reducing Unused Space in a File System.
    US Patent 7739312. Filed April, 2007, issued June 2010. Assigned to Network Appliance.
    Colin Stebbins Gordon, Pratap Vikram Singh, and Donald Alvin Trimmer.
    [ Patent at USPTO ]

Service


Industry Experience


  • Microsoft: Technical Strategy Incubation - Intern, Program analysis work. See OOPSLA'12 publication. (Summer 2011)
  • Microsoft: Technical Strategy Incubation - Full Time, Kernel developer on an unannounced systems project. Worked on kernel debugger implementation, interrupt handling, post-mortem debugging, platform abstractions, all work interacting with other subsystems. (August 2008 - September 2009)
  • Sun Microsystems: Solaris Kernel Group - Intern, merged two processor grouping scheduler abstractions. (Summer 2007)
  • NetApp: Filesystems Group - Intern, designed, documented, and implemented special-purpose filesystem. Resulted in two patents, listed above. (Summer 2006)

Honors


Teaching


Interesting Readings