Quora answer: What are the most interesting Microsoft Research papers?
I have been interested for a long time in the work of Yuri Gurevich who is at Microsoft Research and who was the inventor of the Gurevich Abstract State Machine specification method and the ASL language.
http://research.microsoft.com/en-us/um/people/gurevich/
http://www.eecs.umich.edu/gasm/
http://en.wikipedia.org/wiki/Abstract_State_Machine_Language
http://en.wikipedia.org/wiki/Abstract_state_machines
http://books.google.com/books?id=Am43BAC06L8C
http://books.google.com/books?id=HqIRT51n74YC
Gurevich is a Mathematician who proved that a higher order and abstract language could be Turing equivalent so that we did not have to reduce to a Turing machine representation to know that something was Turing computable, and that made it possible to have a very specification language at any given level of abstraction that was assured to be computable. The method is very simple and basically can be described in one sentence which is “Define it with rules.” So a given set of rules that are well-formed at a given level of abstraction can be equivalent to a Turing machine representation of the same algorithm or transformational system. Others such as E. Borger have gone on to turn this into a robust specification method which can describe more types of systems than many other more formal methods while at the same time being easy to use for engineers who seek more formalism in the specification of systems.