publications:
- title: "Intensional polymorphism in type-erasure semantics"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  year: "2002"
  doi: "http://dx.doi.org/10.1017/S0956796801004282"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796801004282"
  tags:
  - "semantics"
  researchr: "https://researchr.org/publication/CraryWM02"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "12"
  number: "6"
  pages: "567-600"
  kind: "article"
  key: "CraryWM02"
- title: "Higher-Order Intensional Type Analysis"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2002"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2305/23050098.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2305/23050098.htm"
  tags:
  - "analysis"
  researchr: "https://researchr.org/publication/Weirich02"
  cites: 0
  citedby: 0
  pages: "98-114"
  booktitle: "Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings"
  editor:
  - name: "Daniel Le Métayer"
    link: "https://researchr.org/alias/daniel-le-m%C3%A9tayer"
  volume: "2305"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-43363-5"
  kind: "inproceedings"
  key: "Weirich02"
- 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: "Safe zero-cost coercions for Haskell"
  author:
  - name: "Joachim Breitner"
    link: "https://researchr.org/alias/joachim-breitner"
  - name: "Richard A. Eisenberg"
    link: "http://cs.brynmawr.edu/~rae"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628141"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628141"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/BreitnerEJW14"
  researchr: "https://researchr.org/publication/BreitnerEJW14"
  cites: 0
  citedby: 0
  pages: "189-202"
  booktitle: "Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014"
  editor:
  - name: "Johan Jeuring"
    link: "https://researchr.org/alias/johan-jeuring"
  - name: "Manuel M. T. Chakravarty"
    link: "https://researchr.org/alias/manuel-m.-t.-chakravarty"
  publisher: "ACM"
  isbn: "978-1-4503-2873-9"
  kind: "inproceedings"
  key: "BreitnerEJW14"
- title: "Intensional Polymorphism in Type-Erasure Semantics"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  year: "1998"
  doi: "http://doi.acm.org/10.1145/289423.289459"
  links:
    doi: "http://doi.acm.org/10.1145/289423.289459"
  tags:
  - "semantics"
  researchr: "https://researchr.org/publication/CraryWM98"
  cites: 0
  citedby: 0
  pages: "301-312"
  booktitle: "Proceedings of the third ACM SIGPLAN international conference on Functional programming"
  editor:
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Paul Hudak"
    link: "http://www.cs.yale.edu/homes/hudak/"
  - name: "Christian Queinnec"
    link: "https://researchr.org/alias/christian-queinnec"
  address: "Baltimore, Maryland, United States"
  publisher: "ACM"
  kind: "inproceedings"
  key: "CraryWM98"
- title: "Dependently typed programming with singletons"
  author:
  - name: "Richard A. Eisenberg"
    link: "http://cs.brynmawr.edu/~rae"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2364506.2364522"
  links:
    doi: "http://doi.acm.org/10.1145/2364506.2364522"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/EisenbergW12"
  researchr: "https://researchr.org/publication/EisenbergW12"
  cites: 0
  citedby: 0
  pages: "117-130"
  booktitle: "Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012, Copenhagen, Denmark, 13 September 2012"
  editor:
  - name: "Janis Voigtländer"
    link: "http://www.iai.uni-bonn.de/~jv/"
  publisher: "ACM"
  isbn: "978-1-4503-1574-6"
  kind: "inproceedings"
  key: "EisenbergW12"
- title: "Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism"
  author:
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/944705.944728"
  links:
    doi: "http://doi.acm.org/10.1145/944705.944728"
  tags:
  - "abstract syntax"
  researchr: "https://researchr.org/publication/WashburnW03"
  cites: 0
  citedby: 0
  pages: "249-262"
  booktitle: "Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003"
  editor:
  - name: "Colin Runciman"
    link: "https://researchr.org/alias/colin-runciman"
  - name: "Olin Shivers"
    link: "https://researchr.org/alias/olin-shivers"
  publisher: "ACM"
  isbn: "1-58113-756-7"
  kind: "inproceedings"
  key: "WashburnW03"
- 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: "A Reflection on Types"
  author:
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Richard A. Eisenberg"
    link: "http://cs.brynmawr.edu/~rae"
  - name: "Dimitrios Vytiniotis"
    link: "https://researchr.org/alias/dimitrios-vytiniotis"
  year: "2016"
  doi: "http://dx.doi.org/10.1007/978-3-319-30936-1_16"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-30936-1_16"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/birthday/JonesWEV16"
  researchr: "https://researchr.org/publication/JonesWEV16"
  cites: 0
  citedby: 0
  pages: "292-317"
  booktitle: "A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday"
  editor:
  - name: "Sam Lindley"
    link: "https://researchr.org/alias/sam-lindley"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  - name: "Philip W. Trinder"
    link: "https://researchr.org/alias/philip-w.-trinder"
  - name: "Donald Sannella"
    link: "https://researchr.org/alias/donald-sannella"
  volume: "9600"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-30935-4"
  kind: "inproceedings"
  key: "JonesWEV16"
- title: "Poly::AML::: a polymorphic aspect-oriented functional programming language"
  author:
  - name: "Daniel S. Dantas"
    link: "https://researchr.org/alias/daniel-s.-dantas"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  - 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/1086365.1086404"
  links:
    doi: "http://doi.acm.org/10.1145/1086365.1086404"
  tags:
  - "programming languages"
  - "object-oriented programming"
  - "functional programming"
  - "aspect oriented programming"
  - "programming"
  - "subject-oriented programming"
  - "feature-oriented programming"
  researchr: "https://researchr.org/publication/DantasWWW05"
  cites: 0
  citedby: 0
  pages: "306-319"
  booktitle: "Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005"
  editor:
  - name: "Olivier Danvy"
    link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  publisher: "ACM"
  isbn: "1-59593-064-7"
  kind: "inproceedings"
  key: "DantasWWW05"
- title: "Visible Type Application"
  author:
  - name: "Richard A. Eisenberg"
    link: "http://cs.brynmawr.edu/~rae"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Hamidhasan G. Ahmed"
    link: "https://researchr.org/alias/hamidhasan-g.-ahmed"
  year: "2016"
  doi: "http://dx.doi.org/10.1007/978-3-662-49498-1_10"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-49498-1_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/EisenbergWA16"
  researchr: "https://researchr.org/publication/EisenbergWA16"
  cites: 0
  citedby: 0
  pages: "229-254"
  booktitle: "Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings"
  editor:
  - name: "Peter Thiemann"
    link: "https://researchr.org/alias/peter-thiemann"
  volume: "9632"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-662-49497-4"
  kind: "inproceedings"
  key: "EisenbergWA16"
- title: "Reactive noninterference"
  author:
  - name: "Aaron Bohannon"
    link: "https://researchr.org/alias/aaron-bohannon"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Vilhelm Sjöberg"
    link: "https://researchr.org/alias/vilhelm-sj%C3%A3%C2%B6berg"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Steve Zdancewic"
    link: "https://researchr.org/alias/steve-zdancewic"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1653662.1653673"
  links:
    doi: "http://doi.acm.org/10.1145/1653662.1653673"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/BohannonPSWZ09"
  cites: 0
  citedby: 0
  pages: "79-90"
  booktitle: "Proceedings of the 2009 ACM Conference on Computer and Communications Security, CCS 2009, Chicago, Illinois, USA, November 9-13, 2009"
  editor:
  - name: "Ehab Al-Shaer"
    link: "https://researchr.org/alias/ehab-al-shaer"
  - name: "Somesh Jha"
    link: "https://researchr.org/alias/somesh-jha"
  - name: "Angelos D. Keromytis"
    link: "https://researchr.org/alias/angelos-d.-keromytis"
  publisher: "ACM"
  isbn: "978-1-60558-894-0"
  kind: "inproceedings"
  key: "BohannonPSWZ09"
- title: "Encoding Intensional Type Analysis"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2001"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2028/20280092.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2028/20280092.htm"
  tags:
  - "analysis"
  researchr: "https://researchr.org/publication/Weirich01"
  cites: 0
  citedby: 0
  pages: "92-106"
  booktitle: "Programming Languages and Systems, 10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings"
  editor:
  - name: "David Sands"
    link: "https://researchr.org/alias/david-sands"
  volume: "2028"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-41862-8"
  kind: "inproceedings"
  key: "Weirich01"
- title: "Type-safe cast"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2004"
  doi: "http://dx.doi.org/10.1017/S0956796804005179"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796804005179"
  researchr: "https://researchr.org/publication/Weirich04"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "14"
  number: "6"
  pages: "681-695"
  kind: "article"
  key: "Weirich04"
- title: "Type-safe cast: functional pearl"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/351240.351246"
  links:
    doi: "http://doi.acm.org/10.1145/351240.351246"
  researchr: "https://researchr.org/publication/Weirich00"
  cites: 0
  citedby: 0
  pages: "58-67"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Weirich00"
- title: "System FC with explicit kind equality"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Justin Hsu"
    link: "https://researchr.org/alias/justin-hsu"
  - name: "Richard A. Eisenberg"
    link: "http://cs.brynmawr.edu/~rae"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2500365.2500599"
  links:
    doi: "http://doi.acm.org/10.1145/2500365.2500599"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/WeirichHE13"
  researchr: "https://researchr.org/publication/WeirichHE13"
  cites: 0
  citedby: 0
  pages: "275-286"
  booktitle: "ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013"
  editor:
  - name: "Greg Morrisett"
    link: "https://researchr.org/alias/greg-morrisett"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  publisher: "ACM"
  isbn: "978-1-4503-2326-0"
  kind: "inproceedings"
  key: "WeirichHE13"
- title: "Generalizing Parametricity Using Information-flow"
  author:
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2005"
  doi: "http://dx.doi.org/10.1109/LICS.2005.20"
  links:
    doi: "http://dx.doi.org/10.1109/LICS.2005.20"
  tags:
  - "data-flow"
  researchr: "https://researchr.org/publication/WashburnW05"
  cites: 0
  citedby: 0
  pages: "62-71"
  booktitle: "20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings"
  publisher: "IEEE Computer Society"
  isbn: "0-7695-2266-1"
  kind: "inproceedings"
  key: "WashburnW05"
- title: "RepLib: a library for derivable type classes"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1159842.1159844"
  links:
    doi: "http://doi.acm.org/10.1145/1159842.1159844"
  tags:
  - "Haskell"
  researchr: "https://researchr.org/publication/Weirich06"
  cites: 0
  citedby: 0
  pages: "1-12"
  booktitle: "Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2006, Portland, Oregon, USA, September 17, 2006"
  editor:
  - name: "Andres Löh"
    link: "http://people.cs.uu.nl/andres/"
  publisher: "ACM"
  isbn: "1-59593-489-8"
  kind: "inproceedings"
  key: "Weirich06"
- title: "Type-safe run-time polytypic programming"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2006"
  doi: "http://dx.doi.org/10.1017/S0956796806005879"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796806005879"
  tags:
  - "polytypic programming"
  - "programming"
  - "polytypic"
  researchr: "https://researchr.org/publication/Weirich06%3A0"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "16"
  number: "6"
  pages: "681-710"
  kind: "article"
  key: "Weirich06:0"
- title: "Nominal Reasoning Techniques in Coq: (Extended Abstract)"
  author:
  - name: "Brian E. Aydemir"
    link: "https://researchr.org/alias/brian-e.-aydemir"
  - name: "Aaron Bohannon"
    link: "https://researchr.org/alias/aaron-bohannon"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.entcs.2007.01.028"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2007.01.028"
  tags:
  - "Coq"
  - "variable binding"
  - "e-science"
  researchr: "https://researchr.org/publication/AydemirBW07"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "174"
  number: "5"
  pages: "69-77"
  kind: "article"
  key: "AydemirBW07"
- title: "Static Debugging: Browsing the Web of Program Invariants"
  author:
  - name: "Cormac Flanagan"
    link: "https://researchr.org/alias/cormac-flanagan"
  - name: "Matthew Flatt"
    link: "http://www.cs.utah.edu/~mflatt/"
  - name: "Shriram Krishnamurthi"
    link: "http://www.cs.brown.edu/~sk/"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  year: "1996"
  tags:
  - "debugging"
  researchr: "https://researchr.org/publication/FlanaganFKWF96"
  cites: 0
  citedby: 0
  pages: "23-32"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "FlanaganFKWF96"
- title: "A Design for Type-Directed Programming in Java"
  author:
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Liang Huang"
    link: "https://researchr.org/alias/liang-huang"
  year: "2005"
  doi: "http://dx.doi.org/10.1016/j.entcs.2005.09.014"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2005.09.014"
  tags:
  - "Java"
  - "programming"
  - "design"
  researchr: "https://researchr.org/publication/WeirichH05"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "138"
  number: "2"
  pages: "117-136"
  kind: "article"
  key: "WeirichH05"
- 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: "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: "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: "It Is Time to Mechanize Programming Language Metatheory"
  author:
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  - 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/978-3-540-69149-5_3"
  abstract: "How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem. We have proposed the POPLMark challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses. "
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-69149-5_3"
  tags:
  - "programming languages"
  - "program verification"
  - "C++"
  - "metatheory"
  - "programming"
  researchr: "https://researchr.org/publication/PierceSWZ05"
  cites: 22
  citedby: 0
  pages: "26-30"
  booktitle: "Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions"
  editor:
  - name: "Bertrand Meyer"
    link: "http://se.ethz.ch/~meyer/"
  - name: "Jim Woodcock"
    link: "https://researchr.org/alias/jim-woodcock"
  volume: "4171"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-540-69147-1"
  kind: "inproceedings"
  key: "PierceSWZ05"
- title: "AspectML: A polymorphic aspect-oriented functional programming language"
  author:
  - name: "Daniel S. Dantas"
    link: "https://researchr.org/alias/daniel-s.-dantas"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1353445.1353448"
  links:
    doi: "http://doi.acm.org/10.1145/1353445.1353448"
  tags:
  - "programming languages"
  - "object-oriented programming"
  - "functional programming"
  - "aspect oriented programming"
  - "programming"
  - "subject-oriented programming"
  - "feature-oriented programming"
  researchr: "https://researchr.org/publication/DantasWWW08"
  cites: 0
  citedby: 0
  journal: "ACM Transactions on Programming Languages and Systems"
  volume: "30"
  number: "3"
  kind: "article"
  key: "DantasWWW08"
- title: "Good advice for type-directed programming aspect-oriented programming and extensible generic functions"
  author:
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1159861.1159867"
  links:
    doi: "http://doi.acm.org/10.1145/1159861.1159867"
  tags:
  - "object-oriented programming"
  - "generic programming"
  - "aspect oriented programming"
  - "programming"
  - "subject-oriented programming"
  - "feature-oriented programming"
  researchr: "https://researchr.org/publication/WashburnW06"
  cites: 0
  citedby: 0
  pages: "33-44"
  booktitle: "Proceedings of the ACM SIGPLAN Workshop on Genetic Programming, WGP 2006, Portland, Oregon, USA, September 16, 2006"
  editor:
  - name: "Ralf Hinze"
    link: "https://researchr.org/alias/ralf-hinze"
  publisher: "ACM"
  kind: "inproceedings"
  key: "WashburnW06"
- title: "Safe and Flexible Dynamic Linking of Native Code"
  author:
  - name: "Michael W. Hicks"
    link: "https://researchr.org/alias/michael-w.-hicks"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  year: "2000"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2071/20710147.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2071/20710147.htm"
  researchr: "https://researchr.org/publication/HicksWC00"
  cites: 0
  citedby: 0
  pages: "147-176"
  booktitle: "Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers"
  editor:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  volume: "2071"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-42196-3"
  kind: "inproceedings"
  key: "HicksWC00"
- title: "Engineering formal metatheory"
  author:
  - name: "Brian E. Aydemir"
    link: "https://researchr.org/alias/brian-e.-aydemir"
  - name: "Arthur Charguéraud"
    link: "https://researchr.org/alias/arthur-chargu%C3%A9raud"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Randy Pollack"
    link: "https://researchr.org/alias/randy-pollack"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1328438.1328443"
  abstract: "Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over existing methodology, leading to developments that are faithful to informal practice, yet require no external tool support and little infrastructure within the proof assistant. We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for and ML (with references, exceptions, datatypes, recursion and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension. "
  links:
    doi: "http://doi.acm.org/10.1145/1328438.1328443"
  tags:
  - "programming languages"
  - "optimization"
  - "object-oriented programming"
  - "Machanized Metatheory"
  - "proof assistant"
  - "pattern language"
  - "type soundness"
  - "exceptions"
  - "Coq"
  - "variable binding"
  - "language engineering"
  - "Cofinite quantification"
  - "principles"
  - "little language"
  - "C++"
  - "metatheory"
  - "programming"
  - "subject-oriented programming"
  - "Syntactic type soundness"
  - "program optimization"
  - "systematic-approach"
  - "feature-oriented programming"
  - "Locally nameless"
  researchr: "https://researchr.org/publication/AydemirCPPW08"
  cites: 0
  citedby: 0
  pages: "3-15"
  booktitle: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008"
  editor:
  - name: "George C. Necula"
    link: "https://researchr.org/alias/george-c.-necula"
  - name: "Philip Wadler"
    link: "http://homepages.inf.ed.ac.uk/wadler/"
  publisher: "ACM"
  isbn: "978-1-59593-689-9"
  kind: "inproceedings"
  key: "AydemirCPPW08"
- title: "Closed type families with overlapping equations"
  author:
  - name: "Richard A. Eisenberg"
    link: "http://cs.brynmawr.edu/~rae"
  - name: "Dimitrios Vytiniotis"
    link: "https://researchr.org/alias/dimitrios-vytiniotis"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2535838.2535856"
  links:
    doi: "http://doi.acm.org/10.1145/2535838.2535856"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/EisenbergVJW14"
  researchr: "https://researchr.org/publication/EisenbergVJW14"
  cites: 0
  citedby: 0
  pages: "671-684"
  booktitle: "The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014"
  editor:
  - name: "Suresh Jagannathan"
    link: "https://researchr.org/alias/suresh-jagannathan"
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  publisher: "ACM"
  isbn: "978-1-4503-2544-8"
  kind: "inproceedings"
  key: "EisenbergVJW14"
- title: "Resource Bound Certification"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/325694.325716"
  links:
    doi: "http://doi.acm.org/10.1145/325694.325716"
  tags:
  - "certification"
  researchr: "https://researchr.org/publication/CraryW00"
  cites: 0
  citedby: 0
  pages: "184-198"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "CraryW00"
- 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: "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: "Contracts made manifest"
  author:
  - name: "Michael Greenberg"
    link: "https://researchr.org/alias/michael-greenberg"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1706299.1706341"
  links:
    doi: "http://doi.acm.org/10.1145/1706299.1706341"
  tags:
  - "contracts"
  - "C++"
  researchr: "https://researchr.org/publication/GreenbergPW10"
  cites: 0
  citedby: 0
  pages: "353-364"
  booktitle: "Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010"
  editor:
  - name: "Manuel V. Hermenegildo"
    link: "https://researchr.org/alias/manuel-v.-hermenegildo"
  - name: "Jens Palsberg"
    link: "https://researchr.org/alias/jens-palsberg"
  publisher: "ACM"
  isbn: "978-1-60558-479-9"
  kind: "inproceedings"
  key: "GreenbergPW10"
- title: "Flexible Type Analysis"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/317636.317906"
  links:
    doi: "http://doi.acm.org/10.1145/317636.317906"
  tags:
  - "analysis"
  researchr: "https://researchr.org/publication/CraryW99"
  cites: 0
  citedby: 0
  pages: "233-248"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "CraryW99"
- title: "Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism"
  author:
  - name: "Geoffrey Washburn"
    link: "https://researchr.org/alias/geoffrey-washburn"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2008"
  doi: "http://dx.doi.org/10.1017/S0956796807006557"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796807006557"
  tags:
  - "HOAS"
  - "System F"
  - "abstract syntax"
  - "variable binding"
  researchr: "https://researchr.org/publication/WashburnW08"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "18"
  number: "1"
  pages: "87-140"
  kind: "article"
  key: "WashburnW08"