Dimitrios Vytiniotis
POST DOC RESEARCHER
.
I am a Post Doc Researcher in the Programming Principles and Tools group. Here is some information about me. I can be reached at dimitris AT microsoft DOT com.
Before joining MSR, I was working towards my PhD on Programming Languages at the University of Pennsylvania.
NEWS: I updated my web page! Also, check this slightly controversial idea.
Recent work @ MSR
- 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
- 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
- Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers, let should not be generalized, July 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
Other work
- 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
