Picture Post Doctoral Fellow
Bio Kostas Arkoudas earned his PhD at the MIT AI Lab, and he is now a PostDoctoral researcher there. As a PhD student, he discovered Denotational Proof Languages (DPLs), a class of languages that seamlessly integrate proof and computation, allowing both for lucid proof presentation and for versatile proof search. He has implemented Athena, a powerful DPL for classical polymorphic multi-sorted first-order logic with equality that includes a higher-order strict functional language with concrete datatypes that admit reasoning by structural induction. He is currently exploring the use of DPLs for very-reliable minimal-trusted-base computation (an idea he calls "certified computation"), modal and temporal DPLs, and the application of DPL-based certified computation to compiler technology. In connection with the latter, he is currently working on a framework for proof-based data flow analysis.
Interests Programming language semantics, logic, type systems, compilers.
Email koud@ai.mit.edu
Phone 617-253-3447
Location NE43-803