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.
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.
A dependently-typed, user-extensible and language-centric
approach to proof assistants, my Ph.D. dissertation, submitted on November
2nd 2012. This is the canonical reference to VeriML presenting its design, metatheory, implementation and examples in detail. (This is an update with better formatting and minor corrections; you can find the official Yale version here.)
- Static and User-Extensible Proof Checking, Antonis Stampoulis and Zhong Shao, POPL 2012, January 25-27, 2012, Philadelphia, PA, USA
VeriML: Typed Computation of Logical
Terms inside a Language with Effects, Antonis Stampoulis
and Zhong Shao, ICFP 2010, September 27-29, 2010,
Baltimore, MD, USA
- Extended Version, the accompanying
technical report of the above paper, that includes all typing
rules and metatheory proofs.
- Ph.D. Defense [PDF], October 15, 2012
- POPL 2012, January 26, 2012, Philadelphia, PA, USA. [pptx]
- TYPES 2011, September 9, 2011, Bergen, Norway. Using VeriML to have an alternative, safely user-extensible conversion rule.
- ICFP 2010 (International Conference on Functional Programming), September 29, 2010, Baltimore, MD, USA
- DTP 2010 (Dependently Typed
Programming Workshop), July 9, 2010, Edinburgh, UK
- VeriML version 0.5. A lot of big and small improvements and changes; the most major ones being that VeriML is now compiled through translation to ML (instead of interpreted) and that there is some inductive definition support.
version 0.3. This reflects VeriML as described in our
POPL 2012 paper.
- VeriML version 0.1. An older version corresponding to our ICFP 2010 paper.
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!
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
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.
Classes in Yale where I have served as a teaching assistant:
Below you can find some things I've programmed throughout the years -- either
as personal projects or as class assignments.
- enRay (source, Linux, Windows), a hardware-accelerated
realtime raytracing engine. Example games with binaries for Windows and Linux: enRay invaders, enRay Tetris.
- Tiger Compiler,
for Zhong Shao's Compilers class, implemented in SML/NJ. Uses an intermediate tree generator
module made by Eric Cheng.
- Haskell CSound wrapper with
GADTs and arrows, for Paul Hudak's Haskell + Music
course. Requires a working copy of Haskore.
- Edsger Compiler, for the
Compilers course at the NTUA, implemented in C++. Compiles a subset of C into
x86 assembly and CIL code for .NET.
- Virtual Mechanics (Windows, Linux i386), a simulator for elementary
physics lab experiments. Developed with Albert Angel, Melina Kourti,
Panagiotis Voulgaris and Christos Dimoulas, for the software engineering course at
the NTUA. Originally meant to be used only for 3D simulation of scripted experiments; later a
rudimentary user interface was added.
- Connect Four, a network-enabled
implementation of the popular board game in Java. Includes a powerful AI