Portrait of Dimitrios Vytiniotis

Dimitrios Vytiniotis

Senior Researcher


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.



PC member: SAS 2015, ITP 2015, FHPC 2014, PLDI SRC 2014, ICFP 2013, OBT 2013, PADL 2013, APLAS 2012, TLDI 2012, POPL 2012, Haskell Symposium 2011


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