Antonis Stampoulis

e-mail: firstname dot lastname at gmail dot com
Programming Languages and Verification group
MIT Computer Science and Artificial Intelligence Laboratory
Office: 32-G888
32 Vassar Street
Cambridge, MA, USA 02138
Research Teaching Programming Other
I am a post-doctoral researcher at the Programming Languages and Verification group in MIT CSAIL, working under the supervision of Adam Chlipala. I have recently completed my PhD at the Department of Computer Science of Yale University, where my advisor was Zhong Shao. My main research interests are in the areas of programming languages, software verification, type systems and mechanized logic. Before coming to the US, I was working with Nikos Papaspyrou at the School of Electrical Engineering and Computer Engineering of the National Technical University of Athens, where I completed my undergraduate studies.
Research

VeriML. My dissertation research at Yale focused on the design, metatheory, implementation and usage of a novel programming language and proof assistant, called VeriML. The language aims to provide a compelling alternative to tactic development compared to existing approaches, by leveraging a rich type system coupled with a rich ML-style programming model. I have also shown how generalizations of features of traditional proof assistants, such as interactive development of proofs and tactics, are a direct consequence of its design. Thus the language can be viewed as a proof assistant in its entirety. Through the addition of a simple staging construct, VeriML provides extensible static checking of proofs and tactics, solving long-standing issues such as having a safe yet user-extensible conversion rule. Because of this support, users are free to extend the 'background reasoning' that the proof assistant uses to handle trivial details with domain-specific sophistication of arbitrary complexity; this simplifies the development of further proofs and automation, yielding an approach to formal proofs closer to informal practice.

Publications:

Talks:

Implementation:

SLAM. During the summer of 2007, I interned with Ella Bounimova and Tom Ball at the Software Reliability Group of Microsoft Research, Redmond. I worked on the SLAM project, a static analysis tool that follows the CEGAR methodology to verify whether Windows device drivers written in C make valid system API calls according to some specification. I designed and implemented a field-sensitive pointer analysis algorithm in OCaml, that replaced the existing pointer analysis in SLAM with great results!

Karooma. During my time working with Prof. Nikos Papaspyrou at the NTUA, I designed a surface language called Karooma, that compiles to the typed intermediate language described in A Type System for Certified Binaries by Shao et al. Karooma is a small first-order language that enables users to annotate their functions with pre- and post-conditions. The programmer only needs to write the simply-typed version of functions, and a simple Prolog-style theorem prover handles the generated proof obligations; ultimately, binaries that carry full proof objects of the associated properties are produced.

Publications:

Teaching

Classes in Yale where I have served as a teaching assistant:

Programming
Below you can find some things I've programmed throughout the years -- either as personal projects or as class assignments.
Other

I'm an avid music fan -- check out my Last.fm page to see what I've been listening to lately!
Links to friends' pages: Erato Kremmyda, Mihalis Maniatakos, Argyro Katsika, Athanasios Bamis, Dominik Bartmanski, Christos Dimoulas, Ioannis Koltsidas, Panagiotis Voulgaris, Albert Angel

This webpage uses the Fontin font from http://www.exljbris.com/.