publications:
- title: "Mechanized Metatheory for the Masses: The PoplMark Challenge"
  author:
  - name: "Brian E. Aydemir"
    link: "https://researchr.org/alias/brian-e.-aydemir"
  - name: "Aaron Bohannon"
    link: "https://researchr.org/alias/aaron-bohannon"
  - name: "Matthew Fairbairn"
    link: "https://researchr.org/alias/matthew-fairbairn"
  - name: "J. Nathan Foster"
    link: "http://www.cs.princeton.edu/~jnfoster/"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Steve Zdancewic"
    link: "https://researchr.org/alias/steve-zdancewic"
  year: "2005"
  doi: "http://dx.doi.org/10.1007/11541868_4"
  abstract: "How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F<:, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research."
  links:
    doi: "http://dx.doi.org/10.1007/11541868_4"
  tags:
  - "programming languages"
  - "rule-based"
  - "variable binding"
  - "principles"
  - "type system"
  - "C++"
  - "metatheory"
  - "subtyping"
  - "programming"
  - "state machines"
  researchr: "https://researchr.org/publication/AydemirBFFPSVWWZ05"
  cites: 0
  citedby: 0
  pages: "50-65"
  booktitle: "Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings"
  editor:
  - name: "Joe Hurd"
    link: "https://researchr.org/alias/joe-hurd"
  - name: "Thomas F. Melham"
    link: "https://researchr.org/alias/thomas-f.-melham"
  volume: "3603"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-28372-2"
  kind: "inproceedings"
  key: "AydemirBFFPSVWWZ05"
- title: "FPH: first-class polymorphism for Haskell"
  author:
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1411204.1411246"
  abstract: "Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting ``first-class'' polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm. "
  links:
    doi: "http://doi.acm.org/10.1145/1411204.1411246"
  tags:
  - "programming languages"
  - "type inference"
  - "completeness"
  - "System F"
  - "MLF"
  - "transformation language"
  - "polymorphism"
  - "Haskell"
  - "type system"
  - "transformation system"
  - "higher-order transformations"
  - "transformation"
  - "program transformation"
  researchr: "https://researchr.org/publication/VytiniotisWJ08"
  cites: 0
  citedby: 0
  pages: "295-306"
  booktitle: "Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008"
  editor:
  - name: "James Hook"
    link: "https://researchr.org/alias/james-hook"
  - name: "Peter Thiemann"
    link: "http://www.informatik.uni-freiburg.de/~thiemann/"
  publisher: "ACM"
  isbn: "978-1-59593-919-7"
  kind: "inproceedings"
  key: "VytiniotisWJ08"
- title: "Simple unification-based type inference for GADTs"
  author:
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1159803.1159811"
  links:
    doi: "http://doi.acm.org/10.1145/1159803.1159811"
  tags:
  - "type inference"
  - "rule-based"
  researchr: "https://researchr.org/publication/JonesVWW06"
  cites: 0
  citedby: 0
  pages: "50-61"
  booktitle: "Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006"
  editor:
  - name: "John H. Reppy"
    link: "http://www.cs.uchicago.edu/people/jhr"
  - name: "Julia L. Lawall"
    link: "http://www.diku.dk/hjemmesider/ansatte/julia/"
  publisher: "ACM"
  isbn: "1-59593-309-3"
  kind: "inproceedings"
  key: "JonesVWW06"
- title: "Free Theorems and Runtime Type Representations"
  author:
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.entcs.2007.02.043"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2007.02.043"
  researchr: "https://researchr.org/publication/VytiniotisW07"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "173"
  pages: "357-373"
  kind: "article"
  key: "VytiniotisW07"
- title: "Practical type inference for arbitrary-rank types"
  author:
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Mark Shields"
    link: "https://researchr.org/alias/mark-shields"
  year: "2007"
  doi: "http://dx.doi.org/10.1017/S0956796806006034"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796806006034"
  tags:
  - "type inference"
  researchr: "https://researchr.org/publication/JonesVWS07"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "17"
  number: "1"
  pages: "1-82"
  kind: "article"
  key: "JonesVWS07"
- title: "An open and shut typecase"
  author:
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1040294.1040296"
  links:
    doi: "http://doi.acm.org/10.1145/1040294.1040296"
  tags:
  - "source-to-source"
  - "open-source"
  researchr: "https://researchr.org/publication/VytiniotisWW05"
  cites: 0
  citedby: 0
  pages: "13-24"
  booktitle: "Proceedings of TLDI 05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005"
  editor:
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Manuel Fähndrich"
    link: "https://researchr.org/alias/manuel-f%C3%A4hndrich"
  publisher: "ACM"
  isbn: "1-58113-999-3"
  kind: "inproceedings"
  key: "VytiniotisWW05"
- title: "Boxy types: inference for higher-rank types and impredicativity"
  author:
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1159803.1159838"
  links:
    doi: "http://doi.acm.org/10.1145/1159803.1159838"
  tags:
  - "type inference"
  researchr: "https://researchr.org/publication/VytiniotisWJ06"
  cites: 0
  citedby: 0
  pages: "251-262"
  booktitle: "Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006"
  editor:
  - name: "John H. Reppy"
    link: "http://www.cs.uchicago.edu/people/jhr"
  - name: "Julia L. Lawall"
    link: "http://www.diku.dk/hjemmesider/ansatte/julia/"
  publisher: "ACM"
  isbn: "1-59593-309-3"
  kind: "inproceedings"
  key: "VytiniotisWJ06"
- title: "OutsideIn(X) Modular type inference with local assumptions"
  author:
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Tom Schrijvers"
    link: "http://users.ugent.be/~tschrijv"
  - name: "Martin Sulzmann"
    link: "https://researchr.org/alias/martin-sulzmann"
  year: "2011"
  abstract: " Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and – perhaps controversially – argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OutsideIn(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OutsideIn(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7."
  tags:
  - "empirical"
  - "programming languages"
  - "type inference"
  - "rule-based"
  - "data-flow language"
  - "constraints"
  - "Haskell"
  - "type system"
  - "data-flow programming"
  - "data-flow"
  - "metatheory"
  - "systematic-approach"
  - "local type inference"
  - "domain-specific language"
  researchr: "https://researchr.org/publication/VytiniotisJSS11"
  cites: 0
  citedby: 0
  journal: "J. Funct. Program."
  volume: "21"
  number: "4-5"
  pages: "333-412"
  kind: "article"
  key: "VytiniotisJSS11"