Semantics and Types for Objects with First-Class Member Names
Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi
  author = "Joe~Gibbs Politz and Arjun Guha
            and Shriram Krishnamurthi",
  title = "Semantics and Types for Objects with 
           First-Class Member Names",
  booktitle = "Foundations of Object-Oriented Languages",
  year = 2012

Objects in many programming languages are indexed by first-class strings, not just first-order names. We define λSob ("Lambda sob"), an object calculus for such languages, and prove its untyped sound- ness using Coq. We then develop a type system for λSobb that is built around string pattern types, which describe (possibly infinite) collections of members. We define subtyping over such types, extend them to handle inheritance, and discuss the relationship between the two. We enrich the type system to recognize tests for whether members are present, and briefly discuss exposed inheritance chains. The resulting language permits the ascription of meaningful types to programs that exploit first-class member names for object-relational mapping, sandboxing, dictionaries, etc. We prove that well-typed programs never signal member-not-found errors, even when they use reflection and first-class member names. We briefly discuss the implementation of these types in a prototype type-checker.