Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Dimitrios Vytiniotis

Dimitrios Vytiniotis
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.

News

  • July 2014: Working on the Ziria language: a new domain-specific language for bit stream and packet processing. In collaboration with Bozidar Radunovic of MSRC S&N group.
  • June 2014: Final version of ICFP 2014 paper on refinement type checking for Haskell. With Niki Vazou, Eric Seidel, Ranjit Jhala of UCSD, and Simon Peyton Jones.

Activities

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

Presentations

Recent work @ MSR

    2014

    2013

    2012

    2011

    2010

    • 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

    2009

    2008

    • 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