Vasileios Koutavas

I'm finishing up my Ph.D. at the College of Computer and Information Science of Northeastern University. Here is my CV: [A4 PDF] [Letter PDF].

Contact Information

Mailing Address:	College of Computer and Information Science Northeastern University 360 Huntington Avenue Boston, MA 02115
Physical Address:	West Village H, Room 308 440 Huntington Avenue Boston, MA 02115 (map)
Telephone:	1 (617) 373-2123
e-mail:	vkoutav at ccs neu edu

For Students

Instructions on how to submit your CSG111 or CSG711 homework.

Publications

• A Mechanized Bisimulation for the Nu-Calculus. Nick Benton and Vasileios Koutavas. Ocotber 2007. Unpublished. [ps] [pdf] [proofs in Coq]
  

• Reasoning About Class Behavior. Vasileios Koutavas and Mitchell Wand.
  Up-to-date version (unpublished): [ps] [pdf]
  Version that appeared in FOOL/WOOD 2007: [ps] [pdf] [bib] [FOOL/WOOD'07 Presentation] (The conclusion that downcasting is a conservative extension is wrong in this version, although the conditions of the bisimulation remain the same when we add downcasting to the language. We are grateful to Andrew Kennedy for pointing this out to us.)

• Bisimulations for Untyped Imperative Objects. Vasileios Koutavas and Mitchell Wand. In Programming Languages and Systems. 15th European Symposium on Programming, ESOP 2006, Vienna, Austria. Lecture Notes in Computer Science, vol. 3924, Springer-Verlag 2006. [ps] [pdf] [bib] [ESOP'06 presentation]

• Small Bisimulations for Reasoning About Higher-Order Imperative Programs. Vasileios Koutavas and Mitchell Wand. In Proceedings of the 33rd Annual ACM Symposium on Principles of Programming Languages, pages 141-152, New York, NY, USA, 2006. ACM Press. [ps] [pdf] [bib] [POPL'06 presentation] [UniBo'06 presentation]

Research

I am a member of the NU Programming Research Laboratory. I work with Mitchell Wand in the field of programming languages. I'm mainly interested in proving programs do what they were intended to do; especially effectful programs. Semantics (operational and denotational), bisimulations, logical relations, logic, and type-systems are some of the tools one can use to do that. Some other things I find interesting, and would like to look more into, are mechanised proofs, model-checking, abstract interpretation, "programming with proofs", concurrency, and aspects.

Before coming to Northeastern, I did some work on Foundational Proof Carrying Code in the Software Engineering Laboratory of National Technical University of Athens, under the guidance of Nikolaos Papaspyrou.

How-To's and Scripts

• How to make Coq and ProofGeneral work in GNU Emacs on Windows: howto page
• Prevent Google and other search engines from indexing a page: short test & howto page.
• Use LaTeX images in a Powerpoint presentation: short howto page & script.
• Unix scripts to move or copy directory trees and rename all Greek (ISO-8859-7) filenames to Greeklish: gr2grlish v1.0 beta. Diomidis Spinellis has a full-featured Greek codepage convertor, which I may use in future verions of this script.

Other

• A of a small subset of PL and SoftEng Conferences some colleagues and I use. You can subscribe to it from here. If you want to be able to add conferences and help make it more complete drop me an email.
• A great source of science jokes and anecdotes!
• And some other jokes: xkcd, Ph.D. comic.
• Learn about the spelling and pronunciation of my name here.
• My birthplace, the island of Kefalonia.
• Software patents in Europe .