| 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. |
