Until last year I was a research faculty member of the cognitive science department of RPI , and a research affiliate at MIT CSAIL. I am currently a senior research scientist at Telcordia Research Labs (formerly Bellcore Labs, more formerly yet part of Bell Labs), working mostly in AI and on applications of formal methods to real-world problems in the telecommunications and network industries. I received my PhD in computer science from MIT in 2000. Prior to that I received a master's degree in computer science, a master's in philosophy, and a bachelor's in computer science with a minor in philosophy (the latter from RPI, in 1993). My dissertation introduced denotational proof languages (DPLs). I also designed and implemented Athena . After my PhD I went to Manhattan briefly to work for a start-up. I returned to MIT and did a PostDoc for 2 years, first in the Dynamic Languages Group at the AI Lab, and then in the Program Analysis Group. My email is konstantine at alum.mit.edu.