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.
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.
- 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
- Christos Gkantsidis, Dimitrios Vytiniotis, Orion Hodson, Dushyanth Narayanan, Florin Dinu, and Antony Rowstron, Rhea: automatic filtering for unstructured cloud storage, in 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI ’13) , NSDI, 4 April 2013
- ANDREW J. KENNEDY and DIMITRIOS VYTINIOTIS, Every bit counts: The binary representation of typed data and programs, in Journal of Functional Programming, vol. 22, no. Special Issue 4-5, pp. 529-573, 2012
- Brent Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, and Dimitrios Vytiniotis, Giving Haskell a Promotion, in Proceedings of TLDI'12, ACM, 2012
- Dimitrios Vytiniotis, Simon Peyton Jones, and José Pedro Magalhães, Equality proofs and deferred type errors: a compiler pearl, in Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, ACM, New York, NY, USA, 2012
- Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann, OutsideIn(X): Modular type inference with local assumptions, in Journal of Functional Programming, Cambridge University Press, September 2011
- Maximilian Bolingbroke, Simon Peyton Jones, and Dimitrios Vytiniotis, Termination Combinators Forever, in Haskell Symposium 2011, ACM, 2011
- Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic, Generative type abstraction and type-level computation, in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages , ACM SIGPLAN, January 2011
- Dimitrios Vytiniotis and Andrew Kennedy, Functional Pearl: Every bit counts, in Proceedings of the 15th ACM SIGPLAN international conference on Functional programming , ACM, September 2010
- Dimitrios Vytiniotis and Stephanie Weirich, Parametricity, type equality, and higher-order polymorphism, in Journal of Functional Programming, Cambridge University Press, April 2010
- Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers, Let Should not be Generalised, in Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, Association for Computing Machinery, Inc., January 2010
- Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, and Dimitrios Vytiniotis, Complete and Decidable Type Inference for GADTs, in Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming , Association for Computing Machinery, Inc., September 2009
- Claudio Russo and Dimitrios Vytiniotis, QML: explicit first-class polymorphism for ML, in Proceedings of the 2009 ACM SIGPLAN workshop on ML , Association for Computing Machinery, Inc., September 2009
- Dimitrios Vytiniotis and Vasileios Koutavas, Relating step-indexed logical relations and bisimulations, no. MSR-TR-2009-25, March 2009
- Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich, FPH: First-class polymorphism for Haskell, in Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming , Association for Computing Machinery, Inc., September 2008
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