The Association for Computing Machinery has awarded the 2013 Turing Award (the Computer Science equivalent of the Nobel Prize Fields Medal Schock Prize) to Leslie Lamport at Microsoft Research for his work on formal specification and verification techniques, specifically the Temporal Logic of Actions and his work on fault tolerance in distributed systems. Not as close to logic as some other Turing Laureates (is that what they’re called?) but still a nice nod to the continued importance of formal methods derived in part from logic in CS. (Oh yeah, he also invented LaTeX.)