I am a researcher at the MSRC PPT group. My interests span programming languages theory and implementation, type systems, theorem proving, semantics, functional programming, and -- of course -- Haskell! I am involved in the design and implementation of the constraint solver underlying GHC's type inference engine. I am also fascinated by using PL techniques such as program analyses or domain-specific languages to optimize systems.

Before joining MSR, I completed my PhD on Programming Languages at the University of Pennsylvania. A long time ago I graduated from the NTUA ECE department in Athens.

I can be reached at dimitris at microsoft dot com

Internship opportunities at MSR Cambridge: Check out our internship info page or send me an email if you would like to work in one of the above areas.

News

• March 2013: Higher-order cardinality analysis (with Ilya Sergey and S. Peyton Jones). Describes an optimizing static analysis in GHC that reduces allocation and runtime for Haskell programs. (draft, including proof sketches)
• March 2013: Testing Noninterference, Quickly (with Catalin Hritcu, John Hughes, Benjamin Pierce, Antal Spector-Zabusky, Arthur Azevedo de Amorim, and Leonidas Lampropoulos). Describes the development of a testing framework for hardware models that support dynamic enforcement of information flow. (draft)
• February 2013: Rhea: automatic filtering for unstructured cloud storage (with Ch. Gkantsidis, O. Hodson, D. Narayanan, A. Rowstron, and Fl. Dinu) (to appear in Usenix NSDI 2013)
• October 2012: HALO: Haskell to Logic through Denotational Semantics (with S. Peyton Jones, Koen Claessen, and Dan Rosén). (to appear in POPL 2013)
• August 2012: The paper Stop when you are Almost-Full: Adventures in Constructive Termination (with Thierry Coquand and David Wahlstedt) which proves size-change termination, Terminator, and termination testing with well-quasi-orders constructively, inside Type Theory was presented at ITP 2012 in Princeton. Here is some Coq code  and the presentation.

Activities

• Submit a paper to ICFP 2013!
• Former PC member: OBT 2013, PADL 2013, APLAS 2012, TLDI 2012, POPL 2012, Haskell Symposium 2011

Recent presentations

• Contract checking for Haskell through FOL semantics, POPL 2013, Rome; also given in some variation at MIT, University of Edinburgh LFCS, and IFIP WG 2.8 meetings in 2012.
• Stop when you are Almost-Full, invited talk at JFLA 2012, ITP 2012, Princeton NJ
• Type-based termination with disjunctive invariants, IFIP WG2.8, Texas, 2011
• Generative type abstraction and type-level computation, POPL 2011, Austin TX
• Every Bit Counts, ICFP 2010, Baltimore, MD
• Let should not be generalized, TLDI 2010, Madrid, Spain
• My old MSR job talk slides, MSR Cambridge, Spring 2010

Older work (2003-2007)

• Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(1):1-82, 2007. (a thorough study of various higher-rank type systems)
• Dimitrios Vytiniotis and Stephanie Weirich. Free theorems and runtime type representations. In M. Fiore and M. Mislove, editors, Proceedings of the 23rd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII), volume 173 of Electronic Notes in Theoretical Computer Science, pages 357-373, 2007 (btw ... YES, representations of function types are included and it's all formalized in Isabelle/HOL!)
• Dimitrios Vytiniotis and Stephanie Weirich. Dependent types: Easy as Pie. In Marco T. Morazan and Henrik Nilsson, editors, Draft Proceedings of the 8th Symposium on Trends in Functional Programming. Dept. of Math and Computer Science, Seton Hall University, TR-SHU-CS-2007-04-1, April 2007. (draft outlining some design choices)
• Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 50-61, New York, NY, USA, 2006. ACM Press. (aka Wobbly types)
• Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: inference for higher-rank types and impredicativity. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 251-262, New York, NY, USA, 2006. ACM Press.
• Nate Foster and Dimitrios Vytiniotis. A Theory of Featherweight Java in Isabelle/HOL. In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. http://afp.sourceforge.net/entries/FeatherweightJava.shtml, March 2006. Formal proof development.
• B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), 2005
• Dimitrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich. An open and shut typecase. In Proceedings of The Second ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 13-24, Long Beach, California, January 2005
• Nikolaos Papaspyrou, Dimitrios Vytiniotis, and Vasileios Koutavas. Logic-enhanced type systems: Programming language support for reasoning about security and other program properties. In Proceedings of the Fourth Panhellenic Logic Symposium, Thessaloniki, July 2003