Luca Cardelli is one of the big guns in programming language theory--consistently producing interesting and important results over several decades. His paper (with Peter Wagner) "On Understanding Types, Data Abstraction, and Polymorphism" which I read as a graduate student deeply influenced me. Cardelli is now at Microsoft Research. He has recent slides (from ECOOP 2007) about his journey into the theory of objects called An Accidental Simula User that are a good read for anyone interested in object-oriented programming. Here's the abstract:

It was a simple choice, really, on an IBM 370 in the 70's, between APL, Fortran, Lisp 1.5, PL/1, COBOL, and Simula'67. Nothing could come close to Simula's combination of strong typing, garbage collection, and proper string processing. Separate compilation (prefix classes) and coroutines were nice bonuses. And then there were these . . . ``objects´´ but, well, nothing is perfect. Hot topics in those days were the freshly invented denotational semantics (which Simula didn't have), formal type systems (which objects didn't have), and abstract data types (which seemed to have confusingly little to do with classes). Still, Simula was the obvious choice to get something done comfortably because, after all, it was an improved Algol. It even had the functional programming feature of call-by-name by default. So, it became my first favorite language, for every reason other than it being object-oriented. The story I am going to tell is the very, very slow realization that Simula was the embodiment of a radically different philosophy of programming, and the gradual and difficult efforts to reconcile that philosophy with the formal methods that were being developed for procedural and functional programming. Along the way, domain theory helped rather unexpectedly, at least for a while. Type theory had to be recast for the task at hand. Landin's lambda-reductionism had to be partially abandoned. Always, there seemed to be a deep fundamental mismatch between objects and procedures, well described by Reynolds, that made any unification impossibly complicated. But in the end, both object-oriented and procedural programming have benefited from the clash of cultures. And the story is far from over yet, as witnessed by the still blooming area of program verification for both procedural and object-oriented languages.