publications:
- title: "A type system for higher-order modules"
  author:
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/640128.604151"
  abstract: "We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class values. Our type system harmonizes design elements from previous work, resulting in a simple, economical account of modular programming. The main unifying principle is the treatment of abstraction mechanisms as computational effects. Our language is the first to provide a complete and practical formalization of all of these critical issues in module system design."
  links:
    doi: "http://doi.acm.org/10.1145/640128.604151"
  tags:
  - "type system"
  researchr: "https://researchr.org/publication/DreyerCH03"
  cites: 0
  citedby: 0
  pages: "236-249"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "DreyerCH03"
- title: "Internal Parametricity for Cubical Type Theory"
  author:
  - name: "Evan Cavallo"
    link: "https://researchr.org/alias/evan-cavallo"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2021"
  doi: "https://doi.org/10.46298/lmcs-17(4:5)2021"
  links:
    doi: "https://doi.org/10.46298/lmcs-17(4:5)2021"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lmcs/CavalloH21"
  researchr: "https://researchr.org/publication/CavalloH21"
  cites: 0
  citedby: 0
  journal: "Logical Methods in Computer Science"
  volume: "17"
  number: "4"
  kind: "article"
  key: "CavalloH21"
- title: "Logical Relations as Types: Proof-Relevant Parametricity for Program Modules"
  author:
  - name: "Jonathan Sterling"
    link: "https://researchr.org/alias/jonathan-sterling"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2021"
  doi: "https://doi.org/10.1145/3474834"
  links:
    doi: "https://doi.org/10.1145/3474834"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jacm/SterlingH21"
  researchr: "https://researchr.org/publication/SterlingH21"
  cites: 0
  citedby: 0
  journal: "Journal of the ACM"
  volume: "68"
  number: "6"
  kind: "article"
  key: "SterlingH21"
- title: "Responsive parallel computation: bridging competitive and cooperative threading"
  author:
  - name: "Stefan K. Muller"
    link: "https://researchr.org/alias/stefan-k.-muller"
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3062341.3062370"
  links:
    doi: "http://doi.acm.org/10.1145/3062341.3062370"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/MullerA017"
  researchr: "https://researchr.org/publication/MullerA017"
  cites: 0
  citedby: 0
  pages: "677-692"
  booktitle: "Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017"
  editor:
  - name: "Albert Cohen 0001"
    link: "https://researchr.org/alias/albert-cohen-0001"
  - name: "Martin T. Vechev"
    link: "https://researchr.org/alias/martin-t.-vechev"
  publisher: "ACM"
  isbn: "978-1-4503-4988-8"
  kind: "inproceedings"
  key: "MullerA017"
- title: "Cache efficient functional algorithms"
  author:
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2776825"
  links:
    doi: "http://doi.acm.org/10.1145/2776825"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/cacm/BlellochH15"
  researchr: "https://researchr.org/publication/BlellochH15"
  cites: 0
  citedby: 0
  journal: "Communications of the ACM"
  volume: "58"
  number: "7"
  pages: "101-108"
  kind: "article"
  key: "BlellochH15"
- title: "Typed Closure Conversion for Recursively-Defined Functions"
  author:
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1997"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#020"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#020"
  researchr: "https://researchr.org/publication/MorrisettH97"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "10"
  pages: "230-241"
  kind: "article"
  key: "MorrisettH97"
- title: "A Framework for Defining Logics"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Furio Honsell"
    link: "https://researchr.org/alias/furio-honsell"
  - name: "Gordon D. Plotkin"
    link: "https://researchr.org/alias/gordon-d.-plotkin"
  year: "1987"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/HarperHP87"
  cites: 0
  citedby: 0
  pages: "194-204"
  booktitle: "Proceedings, Symposium on Logic in Computer Science, 22-25 June 1987, Ithaca, New York, USA"
  publisher: "IEEE Computer Society"
  kind: "inproceedings"
  key: "HarperHP87"
- title: "Structure and Representation in LF"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Donald Sannella"
    link: "http://homepages.inf.ed.ac.uk/dts/"
  - name: "Andrzej Tarlecki"
    link: "https://researchr.org/alias/andrzej-tarlecki"
  year: "1989"
  researchr: "https://researchr.org/publication/HarperST89%3A0"
  cites: 0
  citedby: 0
  pages: "226-237"
  booktitle: "Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA"
  publisher: "IEEE Computer Society"
  kind: "inproceedings"
  key: "HarperST89:0"
- title: "The PsyGrid Experience: Using Web Services in the Study of Schizophrenia"
  author:
  - name: "John D. Ainsworth"
    link: "https://researchr.org/alias/john-d.-ainsworth"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2007"
  doi: "http://www.igi-global.com/Bookstore/Article.aspx?TitleId=2201"
  links:
    doi: "http://www.igi-global.com/Bookstore/Article.aspx?TitleId=2201"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/ijhisi/AinsworthH07"
  tags:
  - "web service"
  - "web services"
  researchr: "https://researchr.org/publication/AinsworthH07"
  cites: 0
  citedby: 0
  journal: "IJHISI"
  volume: "2"
  number: "2"
  pages: "1-20"
  kind: "article"
  key: "AinsworthH07"
- title: "Space profiling for parallel functional programs"
  author:
  - name: "Daniel Spoonhower"
    link: "https://researchr.org/alias/daniel-spoonhower"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Phillip B. Gibbons"
    link: "https://researchr.org/alias/phillip-b.-gibbons"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1411204.1411240"
  links:
    doi: "http://doi.acm.org/10.1145/1411204.1411240"
  tags:
  - "functional programming"
  - "parallel programming"
  - "e-science"
  researchr: "https://researchr.org/publication/SpoonhowerBHG08"
  cites: 0
  citedby: 0
  pages: "253-264"
  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: "SpoonhowerBHG08"
- title: "Correcting computer-based assessments for guessing"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://dx.doi.org/10.1046/j.0266-4909.2002.00001.x"
  links:
    doi: "http://dx.doi.org/10.1046/j.0266-4909.2002.00001.x"
  tags:
  - "rule-based"
  researchr: "https://researchr.org/publication/Harper03%3A2"
  cites: 0
  citedby: 0
  journal: "J. Comp. Assisted Learning"
  volume: "19"
  number: "1"
  pages: "2-8"
  kind: "article"
  key: "Harper03:2"
- title: "A separation logic for concurrent randomized programs"
  author:
  - name: "Joseph Tassarotti"
    link: "https://researchr.org/alias/joseph-tassarotti"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290377"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290377"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/TassarottiH19"
  researchr: "https://researchr.org/publication/TassarottiH19"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "3"
  kind: "article"
  key: "TassarottiH19"
- title: "Resilient cloud computing"
  author:
  - name: "Valentina Salapura"
    link: "https://researchr.org/alias/valentina-salapura"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "M. Viswanathan"
    link: "https://researchr.org/alias/m.-viswanathan"
  year: "2013"
  doi: "http://dx.doi.org/10.1147/JRD.2013.2266972"
  links:
    doi: "http://dx.doi.org/10.1147/JRD.2013.2266972"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/ibmrd/SalapuraHV13"
  researchr: "https://researchr.org/publication/SalapuraHV13"
  cites: 0
  citedby: 0
  journal: "IBM Journal of Research and Development"
  volume: "57"
  number: "5"
  kind: "article"
  key: "SalapuraHV13"
- title: "A Simplified Account of Polymorphic References"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1994"
  researchr: "https://researchr.org/publication/Harper94"
  cites: 0
  citedby: 0
  journal: "Inf. Process. Lett."
  volume: "51"
  number: "4"
  pages: "201-206"
  kind: "article"
  key: "Harper94"
- title: "PET and the IEEE 488 bus (GPIB): Eugene Fisher & Jensen, Osborne/McGraw-Hill (1980) 233 pp £10.00"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1981"
  doi: "http://dx.doi.org/10.1016/0141-9331(81)90529-9"
  links:
    doi: "http://dx.doi.org/10.1016/0141-9331(81)90529-9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mam/Harper81"
  researchr: "https://researchr.org/publication/Harper81"
  cites: 0
  citedby: 0
  journal: "Microprocessors and Microsystems"
  volume: "5"
  number: "1"
  pages: "36-37"
  kind: "article"
  key: "Harper81"
- title: "Automatic Generation of Staged Geometric Predicates"
  author:
  - name: "Aleksandar Nanevski"
    link: "https://researchr.org/alias/aleksandar-nanevski"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://dx.doi.org/10.1023/A:1025876920522"
  links:
    doi: "http://dx.doi.org/10.1023/A:1025876920522"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/NanevskiBH03"
  cites: 0
  citedby: 0
  journal: "Higher-Order and Symbolic Computation"
  volume: "16"
  number: "4"
  pages: "379-400"
  kind: "article"
  key: "NanevskiBH03"
- title: "Syntactic Logical Relations for Polymorphic and Recursive Types"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.entcs.2007.02.010"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2007.02.010"
  researchr: "https://researchr.org/publication/CraryH07"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "172"
  pages: "259-299"
  kind: "article"
  key: "CraryH07"
- title: "Definition of standard ML"
  author:
  - name: "Robin Milner"
    link: "https://researchr.org/alias/robin-milner"
  - name: "Mads Tofte"
    link: "https://researchr.org/alias/mads-tofte"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1990"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0069232"
  researchr: "https://researchr.org/publication/0069232"
  cites: 0
  citedby: 0
  publisher: "MIT Press"
  isbn: "978-0-262-63132-7"
  kind: "book"
  key: "0069232"
- title: "Dynamizing static algorithms, with applications to dynamic trees and history independence"
  author:
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Jorge L. Vittes"
    link: "https://researchr.org/alias/jorge-l.-vittes"
  - name: "Shan Leung Maverick Woo"
    link: "https://researchr.org/alias/shan-leung-maverick-woo"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/982792.982871"
  links:
    doi: "http://doi.acm.org/10.1145/982792.982871"
  tags:
  - "history"
  researchr: "https://researchr.org/publication/AcarBHVW04"
  cites: 0
  citedby: 0
  pages: "531-540"
  booktitle: "Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004"
  editor:
  - name: "J. Ian Munro"
    link: "https://researchr.org/alias/j.-ian-munro"
  publisher: "SIAM"
  kind: "inproceedings"
  key: "AcarBHVW04"
- title: "From tele ::::presence:::: to human ::::absence::::: the pragmatic construction of the human in communications systems research"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1671011.1671020"
  links:
    doi: "http://doi.acm.org/10.1145/1671011.1671020"
  researchr: "https://researchr.org/publication/Harper09-0"
  cites: 0
  citedby: 0
  pages: "73-82"
  booktitle: "Proceedings of the 2009 British Computer Society Conference on Human-Computer Interaction, BCS-HCI 2009, Cambridge, United Kingdom, 1-5 September 2009"
  publisher: "ACM"
  kind: "inproceedings"
  key: "Harper09-0"
- title: "The Essence of ML"
  author:
  - name: "John C. Mitchell"
    link: "https://researchr.org/alias/john-c.-mitchell"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1988"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/MitchellH88"
  cites: 0
  citedby: 0
  pages: "28-46"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "MitchellH88"
- title: "A Library for Self-Adjusting Computation"
  author:
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Matthias Blume"
    link: "https://researchr.org/alias/matthias-blume"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Kanat Tangwongsan"
    link: "https://researchr.org/alias/kanat-tangwongsan"
  year: "2006"
  doi: "http://dx.doi.org/10.1016/j.entcs.2005.11.043"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2005.11.043"
  researchr: "https://researchr.org/publication/AcarBBHT06"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "148"
  number: "2"
  pages: "127-154"
  kind: "article"
  key: "AcarBBHT06"
- title: "On equivalence and canonical forms in the LF type theory"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1042038.1042041"
  links:
    doi: "http://doi.acm.org/10.1145/1042038.1042041"
  tags:
  - "type theory"
  researchr: "https://researchr.org/publication/HarperP05"
  cites: 0
  citedby: 0
  journal: "ACM Trans. Comput. Log."
  volume: "6"
  number: "1"
  pages: "61-101"
  kind: "article"
  key: "HarperP05"
- title: "Integrated visual analytics workflow with GeoTime and nSpace VAST 2010 mini challenge 1 award: Outstanding Analysis and Accuracy"
  author:
  - name: "Pascale Proulx"
    link: "https://researchr.org/alias/pascale-proulx"
  - name: "Adeel Khamisa"
    link: "https://researchr.org/alias/adeel-khamisa"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2010"
  doi: "http://dx.doi.org/10.1109/VAST.2010.5653053"
  links:
    doi: "http://dx.doi.org/10.1109/VAST.2010.5653053"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/ProulxKH10"
  tags:
  - "analysis"
  - "workflow"
  researchr: "https://researchr.org/publication/ProulxKH10"
  cites: 0
  citedby: 0
  pages: "273-274"
  booktitle: "Proceedings of the IEEE Conference on Visual Analytics Science and Technology, IEEE VAST 2010, Salt Lake City, Utah, USA, 24-29 October 2010, part of VisWeek 2010"
  publisher: "IEEE"
  kind: "inproceedings"
  key: "ProulxKH10"
- title: "Internal Parametricity for Cubical Type Theory"
  author:
  - name: "Evan Cavallo"
    link: "https://researchr.org/alias/evan-cavallo"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2020"
  doi: "https://doi.org/10.4230/LIPIcs.CSL.2020.13"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.CSL.2020.13"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/Cavallo020"
  researchr: "https://researchr.org/publication/Cavallo020"
  cites: 0
  citedby: 0
  booktitle: "28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain"
  editor:
  - name: "Maribel Fernández"
    link: "https://researchr.org/alias/maribel-fern%C3%A1ndez"
  - name: "Anca Muscholl"
    link: "https://researchr.org/alias/anca-muscholl"
  volume: "152"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik"
  isbn: "978-3-95977-132-0"
  kind: "inproceedings"
  key: "Cavallo020"
- title: "FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://dx.doi.org/10.1017/S0956796808007119"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796808007119"
  tags:
  - "debugging"
  researchr: "https://researchr.org/publication/Harper09"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "19"
  number: "2"
  pages: "262"
  kind: "article"
  key: "Harper09"
- title: "What is a Recursive Module?"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Sidd Puri"
    link: "https://researchr.org/alias/sidd-puri"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/301618.301641"
  abstract: "A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can impede modular programming by forcing mutually-dependent components to be consolidated into a single module. Recently there have been several proposals for module systems that admit cyclic dependencies, but it is not clear how these proposals relate to one another, nor how one might integrate them into an expressive module system such as that of ML.To address this question we provide a type-theoretic analysis of the notion of a recursive module in the context of a \"phase-distinction\" formalism for higher-order module systems. We extend this calculus with a recursive module mechanism and a new form of signature, called a recursively dependent signature, to support the definition of recursive modules. These extensions are justified by an interpretation in terms of more primitive language constructs. This interpretation may also serve as a guide for implementation."
  links:
    doi: "http://doi.acm.org/10.1145/301618.301641"
  researchr: "https://researchr.org/publication/CraryHP99"
  cites: 0
  citedby: 0
  pages: "50-63"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "CraryHP99"
- title: "Towards a mechanized metatheory of standard ML"
  author:
  - name: "Daniel K. Lee"
    link: "https://researchr.org/alias/daniel-k.-lee"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1190216.1190245"
  abstract: "We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest. "
  links:
    doi: "http://doi.acm.org/10.1145/1190216.1190245"
  tags:
  - "programming languages"
  - "semantics"
  - "program verification"
  - "exceptions"
  - "metatheory"
  - "programming"
  - "abstraction"
  researchr: "https://researchr.org/publication/LeeCH07%3A0"
  cites: 0
  citedby: 0
  pages: "173-184"
  booktitle: "Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007"
  editor:
  - name: "Martin Hofmann"
    link: "https://researchr.org/alias/martin-hofmann"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  publisher: "ACM"
  isbn: "1-59593-575-4"
  kind: "inproceedings"
  key: "LeeCH07:0"
- title: "Modular type classes"
  author:
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Manuel M. T. Chakravarty"
    link: "https://researchr.org/alias/manuel-m.-t.-chakravarty"
  - name: "Gabriele Keller"
    link: "https://researchr.org/alias/gabriele-keller"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1190216.1190229"
  links:
    doi: "http://doi.acm.org/10.1145/1190216.1190229"
  researchr: "https://researchr.org/publication/DreyerHCK07"
  cites: 0
  citedby: 0
  pages: "63-70"
  booktitle: "Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007"
  editor:
  - name: "Martin Hofmann"
    link: "https://researchr.org/alias/martin-hofmann"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  publisher: "ACM"
  isbn: "1-59593-575-4"
  kind: "inproceedings"
  key: "DreyerHCK07"
- title: "TIL: a type-directed, optimizing compiler for ML (with retrospective)"
  author:
  - name: "David Tarditi"
    link: "https://researchr.org/alias/david-tarditi"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Perry Cheng"
    link: "https://researchr.org/alias/perry-cheng"
  - name: "Christopher A. Stone"
    link: "https://researchr.org/alias/christopher-a.-stone"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  year: "1996"
  doi: "http://doi.acm.org/10.1145/989393.989449"
  links:
    doi: "http://doi.acm.org/10.1145/989393.989449"
  tags:
  - "optimization"
  - "compiler"
  researchr: "https://researchr.org/publication/TarditiMCSHL96a"
  cites: 0
  citedby: 0
  pages: "554-567"
  booktitle: "20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection"
  editor:
  - name: "Kathryn S. McKinley"
    link: "https://researchr.org/alias/kathryn-s.-mckinley"
  publisher: "ACM"
  isbn: "1-58113-623-4"
  kind: "inproceedings"
  key: "TarditiMCSHL96a"
- title: "Strict bidirectional type checking"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  - name: "Leaf Petersen"
    link: "https://researchr.org/alias/leaf-petersen"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1040294.1040301"
  links:
    doi: "http://doi.acm.org/10.1145/1040294.1040301"
  tags:
  - "type checking"
  researchr: "https://researchr.org/publication/ChlipalaPH05"
  cites: 0
  citedby: 0
  pages: "71-78"
  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: "ChlipalaPH05"
- title: "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Kuen-Bang Hou (Favonia)"
    link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2018"
  doi: "https://doi.org/10.4230/LIPIcs.CSL.2018.6"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.CSL.2018.6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/AngiuliF018"
  researchr: "https://researchr.org/publication/AngiuliF018"
  cites: 0
  citedby: 0
  booktitle: "27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK"
  editor:
  - name: "Dan R. Ghica"
    link: "https://researchr.org/alias/dan-r.-ghica"
  - name: "Achim Jung"
    link: "https://researchr.org/alias/achim-jung"
  volume: "119"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik"
  isbn: "978-3-95977-088-0"
  kind: "inproceedings"
  key: "AngiuliF018"
- title: "Syntax and models of Cartesian cubical type theory"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Guillaume Brunerie"
    link: "https://researchr.org/alias/guillaume-brunerie"
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/thierry-coquand"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Kuen-Bang Hou (Favonia)"
    link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  year: "2021"
  doi: "https://doi.org/10.1017/S0960129521000347"
  links:
    doi: "https://doi.org/10.1017/S0960129521000347"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/AngiuliBCHHL21"
  researchr: "https://researchr.org/publication/AngiuliBCHHL21"
  cites: 0
  citedby: 0
  journal: "Mathematical Structures in Computer Science"
  volume: "31"
  number: "4"
  pages: "424-468"
  kind: "article"
  key: "AngiuliBCHHL21"
- title: "Selective memoization"
  author:
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/640128.604133"
  links:
    doi: "http://doi.acm.org/10.1145/640128.604133"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/AcarBH03"
  cites: 0
  citedby: 0
  pages: "14-25"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "AcarBH03"
- title: "An overview of the Oregon programming languages summer school"
  author:
  - name: "Jim Allen"
    link: "https://researchr.org/alias/jim-allen"
  - name: "Zena M. Ariola"
    link: "https://researchr.org/alias/zena-m.-ariola"
  - name: "Pierre-Louis Curien"
    link: "https://researchr.org/alias/pierre-louis-curien"
  - name: "Matthew Fluet"
    link: "https://researchr.org/alias/matthew-fluet"
  - name: "Jeff Foster"
    link: "https://researchr.org/alias/jeff-foster"
  - name: "Dan Grossman"
    link: "https://researchr.org/alias/dan-grossman"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Hugo Herbelin"
    link: "https://researchr.org/alias/hugo-herbelin"
  - name: "Yannis Smaragdakis"
    link: "https://researchr.org/alias/yannis-smaragdakis"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  - name: "Steve Zdancewic"
    link: "https://researchr.org/alias/steve-zdancewic"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1816027.1816029"
  links:
    doi: "http://doi.acm.org/10.1145/1816027.1816029"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/sigplan/AllenACFFGHHSWZ09"
  researchr: "https://researchr.org/publication/AllenACFFGHHSWZ09"
  cites: 0
  citedby: 0
  journal: "SIGPLAN Notices"
  volume: "44"
  number: "11"
  pages: "1-3"
  kind: "article"
  key: "AllenACFFGHHSWZ09"
- title: "Sheaf Semantics of Termination-Insensitive Noninterference"
  author:
  - name: "Jonathan Sterling"
    link: "https://researchr.org/alias/jonathan-sterling"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2022"
  doi: "https://doi.org/10.4230/LIPIcs.FSCD.2022.5"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.FSCD.2022.5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fscd/Sterling022"
  researchr: "https://researchr.org/publication/Sterling022"
  cites: 0
  citedby: 0
  booktitle: "7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel"
  editor:
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/amy-p.-felty"
  volume: "228"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik"
  isbn: "978-3-95977-233-4"
  kind: "inproceedings"
  key: "Sterling022"
- title: "Development and integration of a Surveillance Monitoring solution to provide earlier detection of the deteriorating patient"
  author:
  - name: "N. Donnelly"
    link: "https://researchr.org/alias/n.-donnelly"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "D. Branagh"
    link: "https://researchr.org/alias/d.-branagh"
  - name: "J. Francey"
    link: "https://researchr.org/alias/j.-francey"
  - name: "H. Easlea"
    link: "https://researchr.org/alias/h.-easlea"
  - name: "V. Faro-Maza"
    link: "https://researchr.org/alias/v.-faro-maza"
  - name: "T. Hunniford"
    link: "https://researchr.org/alias/t.-hunniford"
  - name: "A. Mooney"
    link: "https://researchr.org/alias/a.-mooney"
  - name: "J. McLaughlin"
    link: "https://researchr.org/alias/j.-mclaughlin"
  year: "2015"
  doi: "http://dx.doi.org/10.1109/EMBC.2015.7318581"
  links:
    doi: "http://dx.doi.org/10.1109/EMBC.2015.7318581"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/embc/DonnellyHBFEFHM15"
  researchr: "https://researchr.org/publication/DonnellyHBFEFHM15"
  cites: 0
  citedby: 0
  pages: "1198-1202"
  booktitle: "37th Annual International Conference of the IEEE Engineering in Medicine and Biology Society, EMBC 2015, Milan, Italy, August 25-29, 2015"
  publisher: "IEEE"
  isbn: "978-1-4244-9271-8"
  kind: "inproceedings"
  key: "DonnellyHBFEFHM15"
- title: "PsyGrid: Applying e-Science to Epidemiology"
  author:
  - name: "John Ainsworth"
    link: "https://researchr.org/alias/john-ainsworth"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Ismael Juma"
    link: "https://researchr.org/alias/ismael-juma"
  - name: "Iain E. Buchan"
    link: "https://researchr.org/alias/iain-e.-buchan"
  year: "2006"
  doi: "http://doi.ieeecomputersociety.org/10.1109/CBMS.2006.135"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/CBMS.2006.135"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/AinsworthHJB06"
  cites: 0
  citedby: 0
  pages: "727-732"
  booktitle: "19th IEEE International Symposium on Computer-Based Medical Systems (CBMS 2006), 22-23 June 2006, Salt Lake City, Utah, USA"
  publisher: "IEEE Computer Society"
  kind: "inproceedings"
  key: "AinsworthHJB06"
- title: "Self-adjusting beat detection and prediction in music"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "M. Ed Jernigan"
    link: "https://researchr.org/alias/m.-ed-jernigan"
  year: "2004"
  doi: "http://dx.doi.org/10.1109/ICASSP.2004.1326809"
  links:
    doi: "http://dx.doi.org/10.1109/ICASSP.2004.1326809"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icassp/HarperJ04"
  researchr: "https://researchr.org/publication/HarperJ04"
  cites: 0
  citedby: 0
  pages: "245-248"
  booktitle: "2004 IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 2004, Montreal, Quebec, Canada, May 17-21, 2004"
  publisher: "IEEE"
  isbn: "0-7803-8484-9"
  kind: "inproceedings"
  key: "HarperJ04"
- title: "A separate compilation extension to standard ML"
  author:
  - name: "David Swasey"
    link: "https://researchr.org/alias/david-swasey"
  - name: "Tom Murphy VII"
    link: "https://researchr.org/alias/tom-murphy-vii"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1159876.1159883"
  links:
    doi: "http://doi.acm.org/10.1145/1159876.1159883"
  researchr: "https://researchr.org/publication/SwaseyVCH06"
  cites: 0
  citedby: 0
  pages: "32-42"
  booktitle: "Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006"
  editor:
  - name: "Andrew Kennedy"
    link: "https://researchr.org/alias/andrew-kennedy"
  - name: "François Pottier"
    link: "https://researchr.org/alias/fran%C3%A7ois-pottier"
  publisher: "ACM"
  isbn: "1-59593-483-9"
  kind: "inproceedings"
  key: "SwaseyVCH06"
- title: "On the unusual effectiveness of logic in computer science"
  author:
  - name: "Joseph Y. Halpern"
    link: "https://researchr.org/alias/joseph-y.-halpern"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Neil Immerman"
    link: "https://researchr.org/alias/neil-immerman"
  - name: "Phokion G. Kolaitis"
    link: "https://researchr.org/alias/phokion-g.-kolaitis"
  - name: "Moshe Y. Vardi"
    link: "https://researchr.org/alias/moshe-y.-vardi"
  - name: "Victor Vianu"
    link: "https://researchr.org/alias/victor-vianu"
  year: "2001"
  doi: "http://www.math.ucla.edu/~asl/bsl/0702/0702-003.ps"
  links:
    doi: "http://www.math.ucla.edu/~asl/bsl/0702/0702-003.ps"
  tags:
  - "e-science"
  - "logic"
  researchr: "https://researchr.org/publication/HalpernHIKVV01"
  cites: 0
  citedby: 0
  journal: "Bulletin of Symbolic Logic"
  volume: "7"
  number: "2"
  pages: "213-236"
  kind: "article"
  key: "HalpernHIKVV01"
- title: "Adaptive functional programming"
  author:
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2002"
  doi: "http://doi.acm.org/10.1145/503272.503296"
  links:
    doi: "http://doi.acm.org/10.1145/503272.503296"
  tags:
  - "functional programming"
  - "e-science"
  - "programming"
  researchr: "https://researchr.org/publication/AcarBH02"
  cites: 0
  citedby: 0
  pages: "247-259"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "AcarBH02"
- title: "Avian Flu Case Study with nSpace and GeoTime"
  author:
  - name: "Pascale Proulx"
    link: "https://researchr.org/alias/pascale-proulx"
  - name: "Sumeet Tandon"
    link: "https://researchr.org/alias/sumeet-tandon"
  - name: "Adam Bodnar"
    link: "https://researchr.org/alias/adam-bodnar"
  - name: "David Schroh"
    link: "https://researchr.org/alias/david-schroh"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "William Wright"
    link: "https://researchr.org/alias/william-wright"
  year: "2006"
  doi: "http://dx.doi.org/10.1109/VAST.2006.261427"
  links:
    doi: "http://dx.doi.org/10.1109/VAST.2006.261427"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/ProulxTBSHW06"
  tags:
  - "case study"
  researchr: "https://researchr.org/publication/ProulxTBSHW06"
  cites: 0
  citedby: 0
  pages: "27-34"
  booktitle: "IEEE Symposium On Visual Analytics Science And Technology, IEEE VAST 2006, October 31-November 2, 2006, Baltimore, Maryland, USA"
  editor:
  - name: "Pak Chung Wong"
    link: "https://researchr.org/alias/pak-chung-wong"
  - name: "Daniel A. Keim"
    link: "https://researchr.org/alias/daniel-a.-keim"
  publisher: "IEEE"
  isbn: "1-4244-0591-2"
  kind: "inproceedings"
  key: "ProulxTBSHW06"
- title: "Practical Foundations for Programming Languages"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2012"
  links:
    "pdf": "http://www.cs.cmu.edu/~rwh/plbook/book.pdf"
  tags:
  - "programming languages"
  researchr: "https://researchr.org/publication/Harper2012"
  cites: 0
  citedby: 0
  kind: "book"
  key: "Harper2012"
- title: "Using page residency to balance tradeoffs in tracing garbage collection"
  author:
  - name: "Daniel Spoonhower"
    link: "https://researchr.org/alias/daniel-spoonhower"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1064979.1064989"
  links:
    doi: "http://doi.acm.org/10.1145/1064979.1064989"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/SpoonhowerBH05"
  cites: 0
  citedby: 0
  pages: "57-67"
  booktitle: "Proceedings of the 1st International Conference on Virtual Execution Environments, VEE 2005, Chicago, IL, USA, June 11-12, 2005"
  editor:
  - name: "Michael Hind"
    link: "https://researchr.org/alias/michael-hind"
  - name: "Jan Vitek"
    link: "http://www.cs.purdue.edu/homes/jv"
  publisher: "ACM"
  isbn: "1-59593-047-7"
  kind: "inproceedings"
  key: "SpoonhowerBH05"
- title: "Position paper: practical foundations for lrogramming languages"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1480828.1480843"
  links:
    doi: "http://doi.acm.org/10.1145/1480828.1480843"
  researchr: "https://researchr.org/publication/Harper08"
  cites: 0
  citedby: 0
  journal: "SIGPLAN Notices"
  volume: "43"
  number: "11"
  pages: "71-73"
  kind: "article"
  key: "Harper08"
- title: "A Record Calculus Based on Symmetric Concatenation"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  year: "1991"
  tags:
  - "rule-based"
  - "C++"
  researchr: "https://researchr.org/publication/HarperP91%3A0"
  cites: 0
  citedby: 0
  pages: "131-142"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "HarperP91:0"
- title: "Type Checking with Universes"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Robert Pollack"
    link: "https://researchr.org/alias/robert-pollack"
  year: "1991"
  tags:
  - "type checking"
  researchr: "https://researchr.org/publication/HarperP91"
  cites: 0
  citedby: 0
  journal: "Theoretical Computer Science"
  volume: "89"
  number: "1"
  pages: "107-136"
  kind: "article"
  key: "HarperP91"
- title: "Typing First-Class Continuations in ML"
  author:
  - name: "Bruce F. Duba"
    link: "https://researchr.org/alias/bruce-f.-duba"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "David B. MacQueen"
    link: "https://researchr.org/alias/david-b.-macqueen"
  year: "1991"
  researchr: "https://researchr.org/publication/DubaHM91"
  cites: 0
  citedby: 0
  pages: "163-173"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "DubaHM91"
- title: "Focusing on Binding and Computation"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Noam Zeilberger"
    link: "https://researchr.org/alias/noam-zeilberger"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2008"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48"
  researchr: "https://researchr.org/publication/LicataZH08"
  cites: 0
  citedby: 0
  pages: "241-252"
  booktitle: "Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA"
  publisher: "IEEE Computer Society"
  isbn: "978-0-7695-3183-0"
  kind: "inproceedings"
  key: "LicataZH08"
- title: "Correctness of compiling polymorphism to dynamic typing"
  author:
  - name: "Kuen-Bang Hou (Favonia)"
    link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29"
  - name: "Nick Benton"
    link: "https://researchr.org/alias/nick-benton"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2017"
  doi: "http://dx.doi.org/10.1017/S0956796816000265"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000265"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/HouBH17"
  researchr: "https://researchr.org/publication/HouBH17"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "27"
  kind: "article"
  key: "HouBH17"
- title: "How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler"
  author:
  - name: "Andrew Bernard"
    link: "https://researchr.org/alias/andrew-bernard"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  year: "1998"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1473/14730053.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1473/14730053.htm"
  tags:
  - "compiler"
  researchr: "https://researchr.org/publication/BernardHL98"
  cites: 0
  citedby: 0
  pages: "53-77"
  booktitle: "Types in Compilation, Second International Workshop, TIC  98, Kyoto, Japan, March 25-27, 1998, Proceedings"
  editor:
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  - name: "Atsushi Ohori"
    link: "https://researchr.org/alias/atsushi-ohori"
  volume: "1473"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-64925-5"
  kind: "inproceedings"
  key: "BernardHL98"
- title: "Polymorphic Type Assignment and CPS Conversion"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Mark Lillibridge"
    link: "https://researchr.org/alias/mark-lillibridge"
  year: "1993"
  researchr: "https://researchr.org/publication/HarperL93%3A0"
  cites: 0
  citedby: 0
  journal: "Higher-Order and Symbolic Computation"
  volume: "6"
  number: "3-4"
  pages: "361-380"
  kind: "article"
  key: "HarperL93:0"
- title: "ML and Beyond"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "John C. Mitchell"
    link: "https://researchr.org/alias/john-c.-mitchell"
  year: "1996"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperM96"
  cites: 0
  citedby: 0
  journal: "ACM Computing Surveys"
  volume: "28"
  number: "4es"
  pages: "219"
  kind: "article"
  key: "HarperM96"
- title: "Abstract Models of Memory Management"
  author:
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1995"
  tags:
  - "meta-model"
  - "memory management"
  - "Meta-Environment"
  researchr: "https://researchr.org/publication/MorrisettFH95"
  cites: 0
  citedby: 0
  pages: "66-77"
  booktitle: "FPCA"
  kind: "inproceedings"
  key: "MorrisettFH95"
- title: "Stories in GeoTime"
  author:
  - name: "Ryan Eccles"
    link: "https://researchr.org/alias/ryan-eccles"
  - name: "Thomas Kapler"
    link: "https://researchr.org/alias/thomas-kapler"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "William Wright"
    link: "https://researchr.org/alias/william-wright"
  year: "2007"
  doi: "http://dx.doi.org/10.1109/VAST.2007.4388992"
  links:
    doi: "http://dx.doi.org/10.1109/VAST.2007.4388992"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/EcclesKHW07"
  researchr: "https://researchr.org/publication/EcclesKHW07"
  cites: 0
  citedby: 0
  pages: "19-26"
  booktitle: "Proceedings of the IEEE Symposium on Visual Analytics Science and Technology, IEEE VAST 2007, Sacramento, California, USA, October 30-November 1, 2007"
  publisher: "IEEE"
  isbn: "978-1-4244-1659-2"
  kind: "inproceedings"
  key: "EcclesKHW07"
- title: "Configurable Spaces: Temporal analysis in diagrammatic contexts"
  author:
  - name: "Thomas Kapler"
    link: "https://researchr.org/alias/thomas-kapler"
  - name: "Ryan Eccles"
    link: "https://researchr.org/alias/ryan-eccles"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "William Wright"
    link: "https://researchr.org/alias/william-wright"
  year: "2008"
  doi: "http://dx.doi.org/10.1109/VAST.2008.4677355"
  links:
    doi: "http://dx.doi.org/10.1109/VAST.2008.4677355"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/KaplerEHW08"
  tags:
  - "analysis"
  - "context-aware"
  researchr: "https://researchr.org/publication/KaplerEHW08"
  cites: 0
  citedby: 0
  pages: "43-50"
  booktitle: "Proceedings of the IEEE Symposium on Visual Analytics Science and Technology, IEEE VAST 2008, Columbus, Ohio, USA, 19-24 October 2008"
  publisher: "IEEE"
  kind: "inproceedings"
  key: "KaplerEHW08"
- title: "Exception tracking in an open world"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2018"
  doi: "https://doi.org/10.1016/j.tcs.2018.02.032"
  links:
    doi: "https://doi.org/10.1016/j.tcs.2018.02.032"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tcs/Harper18"
  researchr: "https://researchr.org/publication/Harper18"
  cites: 0
  citedby: 0
  journal: "Theoretical Computer Science"
  volume: "741"
  pages: "25-31"
  kind: "article"
  key: "Harper18"
- title: "Cache and I/O efficent functional algorithms"
  author:
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2429069.2429077"
  links:
    doi: "http://doi.acm.org/10.1145/2429069.2429077"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/BlellochH13"
  researchr: "https://researchr.org/publication/BlellochH13"
  cites: 0
  citedby: 0
  pages: "39-50"
  booktitle: "The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013"
  editor:
  - name: "Roberto Giacobazzi"
    link: "https://researchr.org/alias/roberto-giacobazzi"
  - name: "Radhia Cousot"
    link: "https://researchr.org/alias/radhia-cousot"
  publisher: "ACM"
  isbn: "978-1-4503-1832-7"
  kind: "inproceedings"
  key: "BlellochH13"
- title: "A universe of binding and computation"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596550.1596571"
  links:
    doi: "http://doi.acm.org/10.1145/1596550.1596571"
  researchr: "https://researchr.org/publication/LicataH09"
  cites: 0
  citedby: 0
  pages: "123-134"
  booktitle: "Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009"
  editor:
  - name: "Graham Hutton"
    link: "https://researchr.org/alias/graham-hutton"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  publisher: "ACM"
  isbn: "978-1-60558-332-7"
  kind: "inproceedings"
  key: "LicataH09"
- title: "An effective theory of type refinements"
  author:
  - name: "Yitzhak Mandelbaum"
    link: "https://researchr.org/alias/yitzhak-mandelbaum"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/944746.944725"
  links:
    doi: "http://doi.acm.org/10.1145/944746.944725"
  tags:
  - "refinement"
  - "type theory"
  researchr: "https://researchr.org/publication/MandelbaumWH03-0"
  cites: 0
  citedby: 0
  journal: "SIGPLAN Notices"
  volume: "38"
  number: "9"
  pages: "213-225"
  kind: "article"
  key: "MandelbaumWH03-0"
- title: "nSpace and GeoTime: A VAST 2006 Case Study"
  author:
  - name: "Pascale Proulx"
    link: "https://researchr.org/alias/pascale-proulx"
  - name: "Lynn Chien"
    link: "https://researchr.org/alias/lynn-chien"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "David Schroh"
    link: "https://researchr.org/alias/david-schroh"
  - name: "Thomas Kapler"
    link: "https://researchr.org/alias/thomas-kapler"
  - name: "David Jonker"
    link: "https://researchr.org/alias/david-jonker"
  - name: "William Wright"
    link: "https://researchr.org/alias/william-wright"
  year: "2007"
  doi: "http://doi.ieeecomputersociety.org/10.1109/MCG.2007.131"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/MCG.2007.131"
  tags:
  - "case study"
  researchr: "https://researchr.org/publication/ProulxCHSKJW07"
  cites: 0
  citedby: 0
  journal: "IEEE Computer Graphics and Applications"
  volume: "27"
  number: "5"
  pages: "46-56"
  kind: "article"
  key: "ProulxCHSKJW07"
- title: "Proof-Directed Debugging"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1999"
  tags:
  - "debugging"
  researchr: "https://researchr.org/publication/Harper99%3A0"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "9"
  number: "4"
  pages: "463-469"
  kind: "article"
  key: "Harper99:0"
- title: "Higher-Order Modules and the Phase Distinction"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "John C. Mitchell"
    link: "https://researchr.org/alias/john-c.-mitchell"
  - name: "Eugenio Moggi"
    link: "https://researchr.org/alias/eugenio-moggi"
  year: "1990"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperMM90"
  cites: 0
  citedby: 0
  pages: "341-354"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "HarperMM90"
- title: "Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report"
  author:
  - name: "Mark W. Bailey"
    link: "https://researchr.org/alias/mark-w.-bailey"
  - name: "Kim B. Bruce"
    link: "https://researchr.org/alias/kim-b.-bruce"
  - name: "Kathleen Fisher"
    link: "http://www.research.att.com/people/Fisher_Kathleen_S"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Stuart Reges"
    link: "https://researchr.org/alias/stuart-reges"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1508865.1508913"
  links:
    doi: "http://doi.acm.org/10.1145/1508865.1508913"
  tags:
  - "programming languages"
  - "programming"
  researchr: "https://researchr.org/publication/BaileyBFHR09"
  cites: 0
  citedby: 0
  pages: "132-133"
  booktitle: "Proceedings of the 40th SIGCSE Technical Symposium on Computer Science Education, SIGCSE 2009, Chattanooga, TN, USA, March 4-7, 2009"
  editor:
  - name: "Sue Fitzgerald"
    link: "https://researchr.org/alias/sue-fitzgerald"
  - name: "Mark Guzdial"
    link: "https://researchr.org/alias/mark-guzdial"
  - name: "Gary Lewandowski"
    link: "https://researchr.org/alias/gary-lewandowski"
  - name: "Steven A. Wolfman"
    link: "https://researchr.org/alias/steven-a.-wolfman"
  publisher: "ACM"
  isbn: "978-1-60558-183-5"
  kind: "inproceedings"
  key: "BaileyBFHR09"
- title: "A Symmetric Modal Lambda Calculus for Distributed Computing"
  author:
  - name: "Tom Murphy VII"
    link: "https://researchr.org/alias/tom-murphy-vii"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2004"
  doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm"
  links:
    doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm"
  researchr: "https://researchr.org/publication/VIICHP04"
  cites: 0
  citedby: 0
  pages: "286-295"
  booktitle: "19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings"
  publisher: "IEEE Computer Society"
  isbn: "0-7695-2192-4"
  kind: "inproceedings"
  key: "VIICHP04"
- title: "Typing First-Class Continuations in ML"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Bruce F. Duba"
    link: "https://researchr.org/alias/bruce-f.-duba"
  - name: "David B. MacQueen"
    link: "https://researchr.org/alias/david-b.-macqueen"
  year: "1993"
  researchr: "https://researchr.org/publication/HarperDM93"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "3"
  number: "4"
  pages: "465-484"
  kind: "article"
  key: "HarperDM93"
- title: "Silent Data Corruption - Myth or reality?"
  author:
  - name: "Cristian Constantinescu"
    link: "https://researchr.org/alias/cristian-constantinescu"
  - name: "Ishwar Parulkar"
    link: "https://researchr.org/alias/ishwar-parulkar"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Sarah Michalak"
    link: "https://researchr.org/alias/sarah-michalak"
  year: "2008"
  doi: "http://dx.doi.org/10.1109/DSN.2008.4630077"
  links:
    doi: "http://dx.doi.org/10.1109/DSN.2008.4630077"
  tags:
  - "data-flow"
  researchr: "https://researchr.org/publication/ConstantinescuPHM08"
  cites: 0
  citedby: 0
  pages: "108-109"
  booktitle: "The 38th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2008, June 24-27, 2008, Anchorage, Alaska, USA, Proceedings"
  publisher: "IEEE Computer Society"
  kind: "inproceedings"
  key: "ConstantinescuPHM08"
- title: "An effective theory of type refinements"
  author:
  - name: "Yitzhak Mandelbaum"
    link: "https://researchr.org/alias/yitzhak-mandelbaum"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/944705.944725"
  links:
    doi: "http://doi.acm.org/10.1145/944705.944725"
  tags:
  - "refinement"
  - "type theory"
  researchr: "https://researchr.org/publication/MandelbaumWH03"
  cites: 0
  citedby: 0
  pages: "213-225"
  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: "MandelbaumWH03"
- title: "2-Dimensional Directed Type Theory"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2011"
  doi: "http://dx.doi.org/10.1016/j.entcs.2011.09.026"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2011.09.026"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/LicataH11"
  researchr: "https://researchr.org/publication/LicataH11"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "276"
  pages: "263-289"
  kind: "article"
  key: "LicataH11"
- title: "Design and implementation of security in a data collection system for epidemiology"
  author:
  - name: "John D. Ainsworth"
    link: "https://researchr.org/alias/john-d.-ainsworth"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Ismael Juma"
    link: "https://researchr.org/alias/ismael-juma"
  - name: "Iain E. Buchan"
    link: "https://researchr.org/alias/iain-e.-buchan"
  year: "2006"
  doi: "http://www.booksonline.iospress.nl/Content/View.aspx?piid=4754"
  links:
    doi: "http://www.booksonline.iospress.nl/Content/View.aspx?piid=4754"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/healthgrid/AinsworthHJB06"
  researchr: "https://researchr.org/publication/AinsworthHJB06-0"
  cites: 0
  citedby: 0
  pages: "348-357"
  booktitle: "Challenges and Opportunities of HealthGrids - Proceedings of Healthgrid 2006, Valencia, Spain, 7-9 June, 2006"
  editor:
  - name: "Vicente Hernández"
    link: "https://researchr.org/alias/vicente-hern%C3%A1ndez"
  - name: "Ignacio Blanquer"
    link: "https://researchr.org/alias/ignacio-blanquer"
  - name: "Tony Solomonides"
    link: "https://researchr.org/alias/tony-solomonides"
  - name: "Vincent Breton"
    link: "https://researchr.org/alias/vincent-breton"
  - name: "Yannick Legré"
    link: "https://researchr.org/alias/yannick-legr%C3%A9"
  volume: "120"
  series: "Studies in Health Technology and Informatics"
  publisher: "IOS Press"
  isbn: "978-1-58603-617-1"
  kind: "inproceedings"
  key: "AinsworthHJB06-0"
- title: "Competitive parallelism: getting your priorities right"
  author:
  - name: "Stefan K. Muller"
    link: "https://researchr.org/alias/stefan-k.-muller"
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2018"
  doi: "https://doi.org/10.1145/3236790"
  links:
    doi: "https://doi.org/10.1145/3236790"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/MullerA018"
  researchr: "https://researchr.org/publication/MullerA018"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "MullerA018"
- title: "A type theory for memory allocation and data layout"
  author:
  - name: "Leaf Petersen"
    link: "https://researchr.org/alias/leaf-petersen"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/640128.604147"
  links:
    doi: "http://doi.acm.org/10.1145/640128.604147"
  tags:
  - "layout"
  - "data-flow"
  - "type theory"
  researchr: "https://researchr.org/publication/PetersenHCP03"
  cites: 0
  citedby: 0
  pages: "172-184"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "PetersenHCP03"
- title: "Research in Programming Languages for Composability, Safety, and Performance"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  year: "1996"
  tags:
  - "programming languages"
  - "programming"
  researchr: "https://researchr.org/publication/HarperL96"
  cites: 0
  citedby: 0
  journal: "ACM Computing Surveys"
  volume: "28"
  number: "4es"
  pages: "195"
  kind: "article"
  key: "HarperL96"
- title: "Automatic Generation of Staged Geometric Predicates"
  author:
  - name: "Aleksandar Nanevski"
    link: "https://researchr.org/alias/aleksandar-nanevski"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2001"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/NanevskiBH01"
  cites: 0
  citedby: 0
  pages: "217-228"
  booktitle: "Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming"
  series: "ICFP '01"
  address: "New York, NY, USA"
  publisher: "Association for Computing Machinery"
  kind: "inproceedings"
  key: "NanevskiBH01"
- title: "Adaptive functional programming"
  author:
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1186634"
  links:
    doi: "http://doi.acm.org/10.1145/1186634"
  tags:
  - "functional programming"
  - "e-science"
  - "programming"
  researchr: "https://researchr.org/publication/AcarBH06"
  cites: 0
  citedby: 0
  journal: "ACM Transactions on Programming Languages and Systems"
  volume: "28"
  number: "6"
  pages: "990-1034"
  kind: "article"
  key: "AcarBH06"
- title: "Stories in GeoTime"
  author:
  - name: "Ryan Eccles"
    link: "https://researchr.org/alias/ryan-eccles"
  - name: "Thomas Kapler"
    link: "https://researchr.org/alias/thomas-kapler"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "William Wright"
    link: "https://researchr.org/alias/william-wright"
  year: "2008"
  doi: "http://dx.doi.org/10.1057/palgrave.ivs.9500173"
  links:
    doi: "http://dx.doi.org/10.1057/palgrave.ivs.9500173"
  researchr: "https://researchr.org/publication/EcclesKHW08"
  cites: 0
  citedby: 0
  journal: "Information Visualization"
  volume: "7"
  number: "1"
  pages: "3-17"
  kind: "article"
  key: "EcclesKHW08"
- title: "A Higher-Order Logic for Concurrent Termination-Preserving Refinement"
  author:
  - name: "Joseph Tassarotti"
    link: "https://researchr.org/alias/joseph-tassarotti"
  - name: "Ralf Jung"
    link: "https://researchr.org/alias/ralf-jung"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2017"
  doi: "http://dx.doi.org/10.1007/978-3-662-54434-1_34"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-54434-1_34"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/TassarottiJ017"
  researchr: "https://researchr.org/publication/TassarottiJ017"
  cites: 0
  citedby: 0
  pages: "909-936"
  booktitle: "Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings"
  editor:
  - name: "Hongseok Yang"
    link: "https://researchr.org/alias/hongseok-yang"
  volume: "10201"
  series: "Lecture Notes in Computer Science"
  isbn: "978-3-662-54434-1"
  kind: "inproceedings"
  key: "TassarottiJ017"
- title: "A Network Protocol Stack in Standard ML"
  author:
  - name: "Edoardo Biagioni"
    link: "https://researchr.org/alias/edoardo-biagioni"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  year: "2001"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/BiagioniHL01"
  cites: 0
  citedby: 0
  journal: "Higher-Order and Symbolic Computation"
  volume: "14"
  number: "4"
  pages: "309-356"
  kind: "article"
  key: "BiagioniHL01"
- title: "ML and Beyond"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "John C. Mitchell"
    link: "https://researchr.org/alias/john-c.-mitchell"
  year: "1997"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperM97"
  cites: 0
  citedby: 0
  journal: "SIGPLAN Notices"
  volume: "32"
  number: "1"
  pages: "80-85"
  kind: "article"
  key: "HarperM97"
- title: "Distributed Control Flow with Classical Modal Logic"
  author:
  - name: "Tom Murphy VII"
    link: "https://researchr.org/alias/tom-murphy-vii"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2005"
  doi: "http://dx.doi.org/10.1007/11538363_6"
  links:
    doi: "http://dx.doi.org/10.1007/11538363_6"
  tags:
  - "modal logic"
  - "data-flow"
  - "logic"
  researchr: "https://researchr.org/publication/VIICH05"
  cites: 0
  citedby: 0
  pages: "51-69"
  booktitle: "Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings"
  editor:
  - name: "C.-H. Luke Ong"
    link: "https://researchr.org/alias/c.-h.-luke-ong"
  volume: "3634"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-28231-9"
  kind: "inproceedings"
  key: "VIICH05"
- title: "Distributed programming with distributed authorization"
  author:
  - name: "Kumar Avijit"
    link: "https://researchr.org/alias/kumar-avijit"
  - name: "Anupam Datta"
    link: "https://researchr.org/alias/anupam-datta"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1708016.1708021"
  links:
    doi: "http://doi.acm.org/10.1145/1708016.1708021"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/AvijitDH10"
  cites: 0
  citedby: 0
  pages: "27-38"
  booktitle: "Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010"
  editor:
  - name: "Andrew Kennedy"
    link: "https://researchr.org/alias/andrew-kennedy"
  - name: "Nick Benton"
    link: "https://researchr.org/alias/nick-benton"
  publisher: "ACM"
  isbn: "978-1-60558-891-9"
  kind: "inproceedings"
  key: "AvijitDH10"
- title: "Typed compilation of recursive datatypes"
  author:
  - name: "Joseph Vanderwaart"
    link: "https://researchr.org/alias/joseph-vanderwaart"
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  - name: "Leaf Petersen"
    link: "https://researchr.org/alias/leaf-petersen"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Perry Cheng"
    link: "https://researchr.org/alias/perry-cheng"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/604174.604187"
  links:
    doi: "http://doi.acm.org/10.1145/604174.604187"
  researchr: "https://researchr.org/publication/VanderwaartDPCHC03"
  cites: 0
  citedby: 0
  pages: "98-108"
  booktitle: "Proceedings of TLDI 03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003"
  editor:
  - name: "Zhong Shao"
    link: "https://researchr.org/alias/zhong-shao"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  publisher: "ACM"
  isbn: "1-58113-649-8"
  kind: "inproceedings"
  key: "VanderwaartDPCHC03"
- title: "Aspects of the Implementation of Type Theory"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1985"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/us/Harper85"
  researchr: "https://researchr.org/publication/us-153"
  cites: 0
  citedby: 0
  school: "Cornell University, USA"
  kind: "phdthesis"
  key: "us-153"
- title: "A Note on   A Simplified Account of Polymorphic References  "
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1996"
  doi: "http://dx.doi.org/10.1016/0020-0190(95)00178-6"
  links:
    doi: "http://dx.doi.org/10.1016/0020-0190(95)00178-6"
  researchr: "https://researchr.org/publication/Harper96"
  cites: 0
  citedby: 0
  journal: "Inf. Process. Lett."
  volume: "57"
  number: "1"
  pages: "15-16"
  kind: "article"
  key: "Harper96"
- title: "Trustless Grid Computing in ConCert"
  author:
  - name: "Bor-Yuh Evan Chang"
    link: "https://researchr.org/alias/bor-yuh-evan-chang"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Margaret DeLap"
    link: "https://researchr.org/alias/margaret-delap"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Jason Liszka"
    link: "https://researchr.org/alias/jason-liszka"
  - name: "Tom Murphy VII"
    link: "https://researchr.org/alias/tom-murphy-vii"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2002"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm"
  researchr: "https://researchr.org/publication/ChangCDHLVP02"
  cites: 0
  citedby: 0
  pages: "112-125"
  booktitle: "Grid Computing - GRID 2002, Third International Workshop, Baltimore, MD, USA, November 18, 2002, Proceedings"
  editor:
  - name: "Manish Parashar"
    link: "https://researchr.org/alias/manish-parashar"
  volume: "2536"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-00133-6"
  kind: "inproceedings"
  key: "ChangCDHLVP02"
- title: "A Module System for a Programming Language Based on the LF Logical Framework"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "1998"
  tags:
  - "programming languages"
  - "rule-based"
  - "programming"
  researchr: "https://researchr.org/publication/HarperP98"
  cites: 0
  citedby: 0
  journal: "Journal of Logic and Computation"
  volume: "8"
  number: "1"
  pages: "5-31"
  kind: "article"
  key: "HarperP98"
- title: "A Framework for Defining Logics"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Furio Honsell"
    link: "https://researchr.org/alias/furio-honsell"
  - name: "Gordon D. Plotkin"
    link: "http://homepages.inf.ed.ac.uk/gdp/"
  year: "1993"
  doi: "http://doi.acm.org/10.1145/138027.138060"
  links:
    doi: "http://doi.acm.org/10.1145/138027.138060"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/HarperHP93"
  cites: 0
  citedby: 0
  journal: "Journal of the ACM"
  volume: "40"
  number: "1"
  pages: "143-184"
  kind: "article"
  key: "HarperHP93"
- title: "On the Type Structure of Standard ML"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "John C. Mitchell"
    link: "https://researchr.org/alias/john-c.-mitchell"
  year: "1993"
  doi: "http://doi.acm.org/10.1145/169701.169696"
  links:
    doi: "http://doi.acm.org/10.1145/169701.169696"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperM93"
  cites: 0
  citedby: 0
  journal: "ACM Transactions on Programming Languages and Systems"
  volume: "15"
  number: "2"
  pages: "211-252"
  kind: "article"
  key: "HarperM93"
- title: "TIL: A Type-Directed Optimizing Compiler for ML"
  author:
  - name: "David Tarditi"
    link: "https://researchr.org/alias/david-tarditi"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Perry Cheng"
    link: "https://researchr.org/alias/perry-cheng"
  - name: "Christopher A. Stone"
    link: "https://researchr.org/alias/christopher-a.-stone"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  year: "1996"
  tags:
  - "optimization"
  - "compiler"
  researchr: "https://researchr.org/publication/TarditiMCSHL96"
  cites: 0
  citedby: 0
  pages: "181-192"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "TarditiMCSHL96"
- title: "Relational Interpretations of Recursive Types in an operational Setting (Summary)"
  author:
  - name: "Lars Birkedal"
    link: "https://researchr.org/alias/lars-birkedal"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1997"
  researchr: "https://researchr.org/publication/BirkedalH97"
  cites: 0
  citedby: 0
  pages: "458-490"
  booktitle: "Theoretical Aspects of Computer Software, Third International Symposium, TACS  97, Sendai, Japan, September 23-26, 1997, Proceedings"
  editor:
  - name: "Martín Abadi"
    link: "https://researchr.org/alias/mart%C3%ADn-abadi"
  - name: "Takayasu Ito"
    link: "https://researchr.org/alias/takayasu-ito"
  volume: "1281"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-63388-X"
  kind: "inproceedings"
  key: "BirkedalH97"
- title: "Logic Representation in LF"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Donald Sannella"
    link: "http://homepages.inf.ed.ac.uk/dts/"
  - name: "Andrzej Tarlecki"
    link: "https://researchr.org/alias/andrzej-tarlecki"
  year: "1989"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/HarperST89"
  cites: 0
  citedby: 0
  pages: "250-272"
  booktitle: "Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings"
  editor:
  - name: "David H. Pitt"
    link: "https://researchr.org/alias/david-h.-pitt"
  - name: "David E. Rydeheard"
    link: "https://researchr.org/alias/david-e.-rydeheard"
  - name: "Peter Dybjer"
    link: "https://researchr.org/alias/peter-dybjer"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  - name: "Axel Poigné"
    link: "https://researchr.org/alias/axel-poign%C3%A9"
  volume: "389"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-51662-X"
  kind: "inproceedings"
  key: "HarperST89"
- title: "Typed Closure Conversion"
  author:
  - name: "Yasuhiko Minamide"
    link: "https://researchr.org/alias/yasuhiko-minamide"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1996"
  doi: "http://doi.acm.org/10.1145/237721.237791"
  links:
    doi: "http://doi.acm.org/10.1145/237721.237791"
  researchr: "https://researchr.org/publication/MinamideMH96"
  cites: 0
  citedby: 0
  pages: "271-283"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "MinamideMH96"
- title: "Mechanizing the meta-theory of programming languages"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1086365.1086396"
  links:
    doi: "http://doi.acm.org/10.1145/1086365.1086396"
  tags:
  - "programming languages"
  - "meta programming"
  - "meta-model"
  - "programming"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/Harper05%3A0"
  cites: 0
  citedby: 0
  pages: "240"
  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: "Harper05:0"
- title: "Microprocessor-based multichannel analyser developed using POLYFORTH"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1983"
  doi: "http://dx.doi.org/10.1016/0141-9331(83)90328-9"
  links:
    doi: "http://dx.doi.org/10.1016/0141-9331(83)90328-9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mam/Harper83"
  researchr: "https://researchr.org/publication/Harper83"
  cites: 0
  citedby: 0
  journal: "Microprocessors and Microsystems"
  volume: "7"
  number: "5"
  pages: "217-222"
  kind: "article"
  key: "Harper83"
- title: "Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures"
  author:
  - name: "Daniel Spoonhower"
    link: "https://researchr.org/alias/daniel-spoonhower"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Phillip B. Gibbons"
    link: "https://researchr.org/alias/phillip-b.-gibbons"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1583991.1584019"
  links:
    doi: "http://doi.acm.org/10.1145/1583991.1584019"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/SpoonhowerBGH09"
  cites: 0
  citedby: 0
  pages: "91-100"
  booktitle: "SPAA 2009: Proceedings of the 21st Annual ACM Symposium on Parallel Algorithms and Architectures, Calgary, Alberta, Canada, August 11-13, 2009"
  editor:
  - name: "Friedhelm Meyer auf der Heide"
    link: "https://researchr.org/alias/friedhelm-meyer-auf-der-heide"
  - name: "Michael A. Bender"
    link: "https://researchr.org/alias/michael-a.-bender"
  publisher: "ACM"
  isbn: "978-1-60558-606-9"
  kind: "inproceedings"
  key: "SpoonhowerBGH09"
- title: "Higher inductive types in cubical computational type theory"
  author:
  - name: "Evan Cavallo"
    link: "https://researchr.org/alias/evan-cavallo"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290314"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290314"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CavalloH19"
  researchr: "https://researchr.org/publication/CavalloH19"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "3"
  kind: "article"
  key: "CavalloH19"
- title: "Self-Adjusting Computation"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2004"
  doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920254abs.htm"
  links:
    doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920254abs.htm"
  researchr: "https://researchr.org/publication/Harper04%3A0"
  cites: 0
  citedby: 0
  pages: "254-255"
  booktitle: "19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings"
  publisher: "IEEE Computer Society"
  isbn: "0-7695-2192-4"
  kind: "inproceedings"
  key: "Harper04:0"
- title: "Consolidating clients on back-end servers with co-location and frequency control"
  author:
  - name: "Yiyu Chen"
    link: "https://researchr.org/alias/yiyu-chen"
  - name: "Amitayu Das"
    link: "https://researchr.org/alias/amitayu-das"
  - name: "Anand Sivasubramaniam"
    link: "https://researchr.org/alias/anand-sivasubramaniam"
  - name: "Qian Wang"
    link: "https://researchr.org/alias/qian-wang"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "M. Bland"
    link: "https://researchr.org/alias/m.-bland"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1140277.1140331"
  links:
    doi: "http://doi.acm.org/10.1145/1140277.1140331"
  researchr: "https://researchr.org/publication/ChenDSWHB06"
  cites: 0
  citedby: 0
  pages: "383-384"
  booktitle: "Proceedings of the Joint International Conference on Measurement and Modeling of Computer Systems, SIGMETRICS/Performance 2006, Saint Malo, France, June 26-30, 2006"
  editor:
  - name: "Raymond A. Marie"
    link: "https://researchr.org/alias/raymond-a.-marie"
  - name: "Peter B. Key"
    link: "https://researchr.org/alias/peter-b.-key"
  - name: "Evgenia Smirni"
    link: "https://researchr.org/alias/evgenia-smirni"
  publisher: "ACM"
  isbn: "1-59593-319-0"
  kind: "inproceedings"
  key: "ChenDSWHB06"
- title: "Positively dependent types"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1481848.1481851"
  links:
    doi: "http://doi.acm.org/10.1145/1481848.1481851"
  researchr: "https://researchr.org/publication/LicataH09-0"
  cites: 0
  citedby: 0
  pages: "3-14"
  booktitle: "Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009"
  editor:
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "Todd D. Millstein"
    link: "https://researchr.org/alias/todd-d.-millstein"
  publisher: "ACM"
  isbn: "978-1-60558-330-3"
  kind: "inproceedings"
  key: "LicataH09-0"
- title: "The past is a different place: they do things differently there"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "D. Randall"
    link: "https://researchr.org/alias/d.-randall"
  - name: "N. Smyth"
    link: "https://researchr.org/alias/n.-smyth"
  - name: "C. Evans"
    link: "https://researchr.org/alias/c.-evans"
  - name: "L. Heledd"
    link: "https://researchr.org/alias/l.-heledd"
  - name: "R. Moore"
    link: "https://researchr.org/alias/r.-moore"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1394445.1394474"
  links:
    doi: "http://doi.acm.org/10.1145/1394445.1394474"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperRSEHM08"
  cites: 0
  citedby: 0
  pages: "271-280"
  booktitle: "Proceedings of the Conference on Designing Interactive Systems, Cape Town, South Africa, February 25-27, 2008"
  editor:
  - name: "Johann van der Schijff"
    link: "https://researchr.org/alias/johann-van-der-schijff"
  - name: "Gary Marsden"
    link: "https://researchr.org/alias/gary-marsden"
  publisher: "ACM"
  isbn: "978-1-60558-002-9"
  kind: "inproceedings"
  key: "HarperRSEHM08"
- title: "Space profiling for parallel functional programs"
  author:
  - name: "Daniel Spoonhower"
    link: "https://researchr.org/alias/daniel-spoonhower"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Phillip B. Gibbons"
    link: "https://researchr.org/alias/phillip-b.-gibbons"
  year: "2008"
  doi: "http://dx.doi.org/10.1017/S0956796810000146"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796810000146"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/SpoonhowerBHG08"
  tags:
  - "functional programming"
  - "parallel programming"
  - "e-science"
  researchr: "https://researchr.org/publication/SpoonhowerBHG08-0"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "20"
  number: "5-6"
  pages: "417-461"
  kind: "article"
  key: "SpoonhowerBHG08-0"
- title: "Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft)"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Robert Pollack"
    link: "https://researchr.org/alias/robert-pollack"
  year: "1989"
  tags:
  - "type checking"
  researchr: "https://researchr.org/publication/HarperP89"
  cites: 0
  citedby: 0
  pages: "241-256"
  booktitle: "TAPSOFT 89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13-17, 1989, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Is"
  editor:
  - name: "Josep Díaz"
    link: "https://researchr.org/alias/josep-d%C3%ADaz"
  - name: "Fernando Orejas"
    link: "https://researchr.org/alias/fernando-orejas"
  volume: "352"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-50940-2"
  kind: "inproceedings"
  key: "HarperP89"
- title: "Advanced module systems: a guide for the perplexed (abstract of invited talk)"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/351240.351252"
  links:
    doi: "http://doi.acm.org/10.1145/351240.351252"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperP00"
  cites: 0
  citedby: 0
  pages: "130"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "HarperP00"
- title: "A Language-Based Approach to Security"
  author:
  - name: "Fred B. Schneider"
    link: "https://researchr.org/alias/fred-b.-schneider"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2001"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2000/20000086.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2000/20000086.htm"
  tags:
  - "rule-based"
  - "security"
  - "systematic-approach"
  researchr: "https://researchr.org/publication/SchneiderMH01"
  cites: 0
  citedby: 0
  pages: "86-101"
  booktitle: "Informatics  - 10 Years Back. 10 Years Ahead"
  editor:
  - name: "Reinhard Wilhelm"
    link: "https://researchr.org/alias/reinhard-wilhelm"
  volume: "2000"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-41635-8"
  kind: "inproceedings"
  key: "SchneiderMH01"
- title: "Homotopical patch theory"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Edward Morehouse"
    link: "https://researchr.org/alias/edward-morehouse"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0956796816000198"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000198"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AngiuliMLH16"
  researchr: "https://researchr.org/publication/AngiuliMLH16"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "26"
  kind: "article"
  key: "AngiuliMLH16"
- title: "A cost-aware logical framework"
  author:
  - name: "Yue Niu"
    link: "https://researchr.org/alias/yue-niu"
  - name: "Jonathan Sterling"
    link: "https://researchr.org/alias/jonathan-sterling"
  - name: "Harrison Grodin"
    link: "https://researchr.org/alias/harrison-grodin"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2022"
  doi: "https://doi.org/10.1145/3498670"
  links:
    doi: "https://doi.org/10.1145/3498670"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/NiuSGH22"
  researchr: "https://researchr.org/publication/NiuSGH22"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "6"
  number: "POPL"
  pages: "1-31"
  kind: "article"
  key: "NiuSGH22"
- title: "Homotopy type theory: unified foundations of mathematics and computation"
  author:
  - name: "Steve Awodey"
    link: "https://researchr.org/alias/steve-awodey"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2728816.2728825"
  links:
    doi: "http://doi.acm.org/10.1145/2728816.2728825"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/siglog/AwodeyH15"
  researchr: "https://researchr.org/publication/AwodeyH15"
  cites: 0
  citedby: 0
  journal: "SIGLOG News"
  volume: "2"
  number: "1"
  pages: "37-44"
  kind: "article"
  key: "AwodeyH15"
- title: "Compiling Polymorphism Using Intensional Type Analysis"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  year: "1995"
  tags:
  - "analysis"
  - "compiler"
  researchr: "https://researchr.org/publication/HarperM95"
  cites: 0
  citedby: 0
  pages: "130-141"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "HarperM95"
- title: "SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations"
  author:
  - name: "Eric Allen"
    link: "https://researchr.org/alias/eric-allen"
  - name: "Mark W. Bailey"
    link: "https://researchr.org/alias/mark-w.-bailey"
  - name: "Rastislav Bodík"
    link: "https://researchr.org/alias/rastislav-bod%C3%ADk"
  - name: "Kim B. Bruce"
    link: "https://researchr.org/alias/kim-b.-bruce"
  - name: "Kathleen Fisher"
    link: "http://www.research.att.com/people/Fisher_Kathleen_S"
  - name: "Stephen N. Freund"
    link: "https://researchr.org/alias/stephen-n.-freund"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Chandra Krintz"
    link: "https://researchr.org/alias/chandra-krintz"
  - name: "Shriram Krishnamurthi"
    link: "http://www.cs.brown.edu/~sk/"
  - name: "James R. Larus"
    link: "https://researchr.org/alias/james-r.-larus"
  - name: "Doug Lea"
    link: "https://researchr.org/alias/doug-lea"
  - name: "Gary T. Leavens"
    link: "https://researchr.org/alias/gary-t.-leavens"
  - name: "Lori L. Pollock"
    link: "https://researchr.org/alias/lori-l.-pollock"
  - name: "Stuart Reges"
    link: "https://researchr.org/alias/stuart-reges"
  - name: "Martin C. Rinard"
    link: "https://researchr.org/alias/martin-c.-rinard"
  - name: "Mark Sheldon"
    link: "https://researchr.org/alias/mark-sheldon"
  - name: "Franklyn A. Turbak"
    link: "https://researchr.org/alias/franklyn-a.-turbak"
  - name: "Mitchell Wand"
    link: "https://researchr.org/alias/mitchell-wand"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1480828.1480831"
  links:
    doi: "http://doi.acm.org/10.1145/1480828.1480831"
  tags:
  - "programming languages"
  - "C++"
  - "programming"
  researchr: "https://researchr.org/publication/AllenBBBFFHKKLLLPRRSTW08"
  cites: 0
  citedby: 0
  journal: "SIGPLAN Notices"
  volume: "43"
  number: "11"
  pages: "6-29"
  kind: "article"
  key: "AllenBBBFFHKKLLLPRRSTW08"
- title: "Editorial"
  author:
  - name: "David A. Basin"
    link: "https://researchr.org/alias/david-a.-basin"
  - name: "Olivier Danvy"
    link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2004"
  doi: "http://dx.doi.org/10.1023/B:LISP.0000029480.20108.7d"
  links:
    doi: "http://dx.doi.org/10.1023/B:LISP.0000029480.20108.7d"
  researchr: "https://researchr.org/publication/BasinDH04"
  cites: 0
  citedby: 0
  journal: "Higher-Order and Symbolic Computation"
  volume: "17"
  number: "3"
  pages: "171"
  kind: "article"
  key: "BasinDH04"
- title: "Verified Tail Bounds for Randomized Programs"
  author:
  - name: "Joseph Tassarotti"
    link: "https://researchr.org/alias/joseph-tassarotti"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-319-94821-8_33"
  links:
    doi: "https://doi.org/10.1007/978-3-319-94821-8_33"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Tassarotti018"
  researchr: "https://researchr.org/publication/Tassarotti018"
  cites: 0
  citedby: 0
  pages: "560-578"
  booktitle: "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings"
  editor:
  - name: "Jeremy Avigad"
    link: "https://researchr.org/alias/jeremy-avigad"
  - name: "Assia Mahboubi"
    link: "https://researchr.org/alias/assia-mahboubi"
  volume: "10895"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-94821-8"
  kind: "inproceedings"
  key: "Tassarotti018"
- title: "The Definition of Standard ML, Revised"
  author:
  - name: "Milner, Robin"
    link: "https://researchr.org/alias/milner%2C-robin"
  - name: "Tofte, Mads"
    link: "https://researchr.org/alias/tofte%2C-mads"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "MacQueen, David"
    link: "https://researchr.org/alias/macqueen%2C-david"
  year: "1997"
  researchr: "https://researchr.org/publication/Milner1997thedefinition"
  cites: 0
  citedby: 0
  address: "Cambridge, MA, USA"
  publisher: "MIT Press"
  kind: "book"
  key: "Milner1997thedefinition"
- title: "A Pronominal Approach to Binding and Computation"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Noam Zeilberger"
    link: "https://researchr.org/alias/noam-zeilberger"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_2"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_2"
  tags:
  - "systematic-approach"
  researchr: "https://researchr.org/publication/HarperLZ09"
  cites: 0
  citedby: 0
  pages: "3-4"
  booktitle: "Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings"
  editor:
  - name: "Pierre-Louis Curien"
    link: "https://researchr.org/alias/pierre-louis-curien"
  volume: "5608"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-02272-2"
  kind: "inproceedings"
  key: "HarperLZ09"
- title: "Automated techniques for provably safe mobile code"
  author:
  - name: "Christopher Colby"
    link: "https://researchr.org/alias/christopher-colby"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2003"
  tags:
  - "mobile code"
  - "mobile"
  researchr: "https://researchr.org/publication/ColbyCHLP03"
  cites: 0
  citedby: 0
  journal: "Theoretical Computer Science"
  volume: "290"
  number: "2"
  pages: "1175-1199"
  kind: "article"
  key: "ColbyCHLP03"
- title: "A Dependently Typed Assembly Language"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2001"
  researchr: "https://researchr.org/publication/XiH01"
  cites: 0
  citedby: 0
  pages: "169-180"
  booktitle: "Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming"
  series: "ICFP '01"
  address: "New York, NY, USA"
  publisher: "Association for Computing Machinery"
  kind: "inproceedings"
  key: "XiH01"
- title: "Structured Theory Presentations and Logic Representations"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Donald Sannella"
    link: "http://homepages.inf.ed.ac.uk/dts/"
  - name: "Andrzej Tarlecki"
    link: "https://researchr.org/alias/andrzej-tarlecki"
  year: "1994"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/HarperST94"
  cites: 0
  citedby: 0
  journal: "Annals of Pure and Applied Logic"
  volume: "67"
  number: "1-3"
  pages: "113-160"
  kind: "article"
  key: "HarperST94"
- title: "Self-Adjusting Computation"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2004"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3142&spage=1"
  links:
    doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3142&spage=1"
  researchr: "https://researchr.org/publication/Harper04"
  cites: 0
  citedby: 0
  pages: "1-2"
  booktitle: "Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings"
  editor:
  - name: "Josep Díaz"
    link: "https://researchr.org/alias/josep-d%C3%ADaz"
  - name: "Juhani Karhumäki"
    link: "https://researchr.org/alias/juhani-karhum%C3%A4ki"
  - name: "Arto Lepistö"
    link: "https://researchr.org/alias/arto-lepist%C3%B6"
  - name: "Donald Sannella"
    link: "http://homepages.inf.ed.ac.uk/dts/"
  volume: "3142"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-22849-7"
  kind: "inproceedings"
  key: "Harper04"
- title: "Type-Safe Distributed Programming with ML5"
  author:
  - name: "Tom Murphy VII"
    link: "https://researchr.org/alias/tom-murphy-vii"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_9"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_9"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/VIICH07"
  cites: 0
  citedby: 0
  pages: "108-123"
  booktitle: "Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers"
  editor:
  - name: "Gilles Barthe"
    link: "https://researchr.org/alias/gilles-barthe"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  volume: "4912"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-540-78662-7"
  kind: "inproceedings"
  key: "VIICH07"
- title: "Relational Interpretations of Recursive Types in an Operational Setting"
  author:
  - name: "Lars Birkedal"
    link: "https://researchr.org/alias/lars-birkedal"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1999"
  researchr: "https://researchr.org/publication/BirkedalH99"
  cites: 0
  citedby: 0
  journal: "Inf. Comput."
  volume: "155"
  number: "1-2"
  pages: "3-63"
  kind: "article"
  key: "BirkedalH99"
- title: "Modules and Persistence in Standard ML"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1985"
  doi: "db/conf/db-workshops/Harper85.html"
  researchr: "https://researchr.org/publication/Harper85"
  cites: 0
  citedby: 0
  pages: "21-30"
  booktitle: "Data Types and Persistence. Edited Papers from the Proceedings of the First Workshop on Persistent Objects, Appin, Scotland, August 1985"
  editor:
  - name: "Malcolm P. Atkinson"
    link: "https://researchr.org/alias/malcolm-p.-atkinson"
  - name: "Peter Buneman"
    link: "https://researchr.org/alias/peter-buneman"
  - name: "Ronald Morrison"
    link: "https://researchr.org/alias/ronald-morrison"
  series: "Topics in Information Systems"
  publisher: "Springer"
  isbn: "3-540-18785-5"
  kind: "inproceedings"
  key: "Harper85"
- title: "Canonicity for 2-dimensional type theory"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2103656.2103697"
  links:
    doi: "http://doi.acm.org/10.1145/2103656.2103697"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/LicataH12"
  researchr: "https://researchr.org/publication/LicataH12"
  cites: 0
  citedby: 0
  pages: "337-348"
  booktitle: "Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012"
  editor:
  - name: "John Field"
    link: "https://researchr.org/alias/john-field"
  - name: "Michael Hicks"
    link: "https://researchr.org/alias/michael-hicks"
  publisher: "ACM"
  isbn: "978-1-4503-1083-3"
  kind: "inproceedings"
  key: "LicataH12"
- title: "Constructing Type Systems over an Operational Semantics"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "1992"
  abstract: "Type theories in the sense of Martin-Löf and the NuPRL system are based on taking as primitive a type-free programming language given by an operational semantics, and defining types as partial equivalence relations on the set of closed terms. The construction of a type system is based on a general form of inductive definition that may either be taken as acceptable in its own right, or further explicated in terms of other patterns of induction. One such account, based on a general theory of inductively-defined relations, was given by Allen. An alternative account, based on an essentially set-theoretic argument, is presented. "
  tags:
  - "programming languages"
  - "semantics"
  - "rule-based"
  - "pattern language"
  - "type system"
  - "programming"
  - "operational semantics"
  - "type theory"
  researchr: "https://researchr.org/publication/Harper92"
  cites: 0
  citedby: 0
  journal: "Journal of Symbolic Computation"
  volume: "14"
  number: "1"
  pages: "71-84"
  kind: "article"
  key: "Harper92"
- title: "Persistent triangulations Journal of Functional Programming"
  author:
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Hal Burch"
    link: "https://researchr.org/alias/hal-burch"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Gary L. Miller"
    link: "https://researchr.org/alias/gary-l.-miller"
  - name: "Noel Walkington"
    link: "https://researchr.org/alias/noel-walkington"
  year: "2001"
  tags:
  - "persistent"
  - "functional programming"
  - "programming"
  researchr: "https://researchr.org/publication/BlellochBCHMW01"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "11"
  number: "5"
  pages: "441-466"
  kind: "article"
  key: "BlellochBCHMW01"
- title: "Homotopical patch theory"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Edward Morehouse"
    link: "https://researchr.org/alias/edward-morehouse"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628158"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628158"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/AngiuliMLH14"
  researchr: "https://researchr.org/publication/AngiuliMLH14"
  cites: 0
  citedby: 0
  pages: "243-256"
  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: "AngiuliMLH14"
- title: "Signatures for a Network Protocol Stack: A Systems Application of Standard ML"
  author:
  - name: "Edoardo Biagioni"
    link: "https://researchr.org/alias/edoardo-biagioni"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  - name: "Brian Milnes"
    link: "https://researchr.org/alias/brian-milnes"
  year: "1994"
  doi: "http://doi.acm.org/10.1145/182409.182431"
  links:
    doi: "http://doi.acm.org/10.1145/182409.182431"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/BiagioniHLM94"
  cites: 0
  citedby: 0
  pages: "55-64"
  booktitle: "LISP and Functional Programming"
  kind: "inproceedings"
  key: "BiagioniHLM94"
- title: "Operational Interpretations of an Extension of F::omega:: with Control Operators"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Mark Lillibridge"
    link: "https://researchr.org/alias/mark-lillibridge"
  year: "1996"
  researchr: "https://researchr.org/publication/HarperL96%3A0"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "6"
  number: "3"
  pages: "393-417"
  kind: "article"
  key: "HarperL96:0"
- title: "Robin Milner 1934--2010: verification, languages, and concurrency"
  author:
  - name: "Andrew D. Gordon"
    link: "https://researchr.org/alias/andrew-d.-gordon"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "John Harrison"
    link: "https://researchr.org/alias/john-harrison"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/1926385.1926439"
  links:
    doi: "http://doi.acm.org/10.1145/1926385.1926439"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/GordonHHJS11"
  researchr: "https://researchr.org/publication/GordonHHJS11"
  cites: 0
  citedby: 0
  pages: "473-474"
  booktitle: "Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011"
  editor:
  - name: "Thomas Ball"
    link: "https://researchr.org/alias/thomas-ball"
  - name: "Mooly Sagiv"
    link: "https://researchr.org/alias/mooly-sagiv"
  publisher: "ACM"
  isbn: "978-1-4503-0490-0"
  kind: "inproceedings"
  key: "GordonHHJS11"
- title: "A Type-Theoretic Approach to Higher-Order Modules with Sharing"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Mark Lillibridge"
    link: "https://researchr.org/alias/mark-lillibridge"
  year: "1994"
  tags:
  - "systematic-approach"
  researchr: "https://researchr.org/publication/HarperL94"
  cites: 0
  citedby: 0
  pages: "123-137"
  booktitle: "Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages"
  kind: "inproceedings"
  key: "HarperL94"
- title: "Parametricity and Variants of Girard s ::::J:::: Operator"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "John C. Mitchell"
    link: "https://researchr.org/alias/john-c.-mitchell"
  year: "1999"
  doi: "http://dx.doi.org/10.1016/S0020-0190(99)00036-8"
  links:
    doi: "http://dx.doi.org/10.1016/S0020-0190(99)00036-8"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperM99"
  cites: 0
  citedby: 0
  journal: "Inf. Process. Lett."
  volume: "70"
  number: "1"
  pages: "1-5"
  kind: "article"
  key: "HarperM99"
- title: "Deciding Type Equivalence with Singleton Kinds"
  author:
  - name: "Christopher A. Stone"
    link: "https://researchr.org/alias/christopher-a.-stone"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/325694.325724"
  links:
    doi: "http://doi.acm.org/10.1145/325694.325724"
  researchr: "https://researchr.org/publication/StoneH00"
  cites: 0
  citedby: 0
  pages: "214-227"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "StoneH00"
- title: "A type-theoretic interpretation of standard ML"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Christopher A. Stone"
    link: "https://researchr.org/alias/christopher-a.-stone"
  year: "2000"
  researchr: "https://researchr.org/publication/HarperS00"
  cites: 0
  citedby: 0
  pages: "341-388"
  booktitle: "Proof, Language, and Interaction, Essays in Honour of Robin Milner"
  editor:
  - name: "Gordon D. Plotkin"
    link: "https://researchr.org/alias/gordon-d.-plotkin"
  - name: "Colin Stirling"
    link: "https://researchr.org/alias/colin-stirling"
  - name: "Mads Tofte"
    link: "https://researchr.org/alias/mads-tofte"
  publisher: "The MIT Press"
  isbn: "978-0-262-16188-6"
  kind: "inproceedings"
  key: "HarperS00"
- title: "A Type Discipline for Program Modules"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Robin Milner"
    link: "https://researchr.org/alias/robin-milner"
  - name: "Mads Tofte"
    link: "https://researchr.org/alias/mads-tofte"
  year: "1987"
  researchr: "https://researchr.org/publication/HarperMT87"
  cites: 0
  citedby: 0
  pages: "308-319"
  booktitle: "TAPSOFT 87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Functional and "
  editor:
  - name: "Hartmut Ehrig"
    link: "https://researchr.org/alias/hartmut-ehrig"
  - name: "Robert A. Kowalski"
    link: "https://researchr.org/alias/robert-a.-kowalski"
  - name: "Giorgio Levi"
    link: "https://researchr.org/alias/giorgio-levi"
  - name: "Ugo Montanari"
    link: "https://researchr.org/alias/ugo-montanari"
  volume: "250"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-17611-X"
  kind: "inproceedings"
  key: "HarperMT87"
- title: "An experimental analysis of self-adjusting computation"
  author:
  - name: "Umut A. Acar"
    link: "https://researchr.org/alias/umut-a.-acar"
  - name: "Guy E. Blelloch"
    link: "https://researchr.org/alias/guy-e.-blelloch"
  - name: "Matthias Blume"
    link: "https://researchr.org/alias/matthias-blume"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Kanat Tangwongsan"
    link: "https://researchr.org/alias/kanat-tangwongsan"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596527.1596530"
  links:
    doi: "http://doi.acm.org/10.1145/1596527.1596530"
  tags:
  - "analysis"
  researchr: "https://researchr.org/publication/AcarBBHT09"
  cites: 0
  citedby: 0
  journal: "ACM Transactions on Programming Languages and Systems"
  volume: "32"
  number: "1"
  kind: "article"
  key: "AcarBBHT09"
- title: "Explicit Polymorphism and CPS Conversion"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Mark Lillibridge"
    link: "https://researchr.org/alias/mark-lillibridge"
  year: "1993"
  researchr: "https://researchr.org/publication/HarperL93"
  cites: 0
  citedby: 0
  pages: "206-219"
  booktitle: "Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"
  kind: "inproceedings"
  key: "HarperL93"
- title: "Generational Stack Collection and Profile-Driven Pretenuring"
  author:
  - name: "Perry Cheng"
    link: "https://researchr.org/alias/perry-cheng"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Peter Lee"
    link: "https://researchr.org/alias/peter-lee"
  year: "1998"
  researchr: "https://researchr.org/publication/ChengHL98"
  cites: 0
  citedby: 0
  pages: "162-173"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "ChengHL98"
- title: "Mechanizing metatheory in a logical framework"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  year: "2007"
  doi: "http://dx.doi.org/10.1017/S0956796807006430"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796807006430"
  tags:
  - "metatheory"
  researchr: "https://researchr.org/publication/HarperL07"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "17"
  number: "4-5"
  pages: "613-673"
  kind: "article"
  key: "HarperL07"
- title: "Higher-order abstract syntax: setting the record straight"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1165555.1165572"
  links:
    doi: "http://doi.acm.org/10.1145/1165555.1165572"
  tags:
  - "abstract syntax"
  researchr: "https://researchr.org/publication/CraryH06"
  cites: 0
  citedby: 0
  journal: "SIGACT News"
  volume: "37"
  number: "3"
  pages: "93-96"
  kind: "article"
  key: "CraryH06"
- title: "Extensional equivalence and singleton types"
  author:
  - name: "Christopher A. Stone"
    link: "https://researchr.org/alias/christopher-a.-stone"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1183278.1183281"
  links:
    doi: "http://doi.acm.org/10.1145/1183278.1183281"
  researchr: "https://researchr.org/publication/StoneH06"
  cites: 0
  citedby: 0
  journal: "ACM Trans. Comput. Log."
  volume: "7"
  number: "4"
  pages: "676-722"
  kind: "article"
  key: "StoneH06"
- title: "Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers"
  year: "2001"
  researchr: "https://researchr.org/publication/tic%3A2000"
  cites: 0
  citedby: 0
  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: "proceedings"
  key: "tic:2000"
- title: "Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), Philadelphia, Pennsylvania, May 24-26, 1996"
  year: "1996"
  note: "SIGPLAN Notices 31(6), June 1996"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/1996"
  researchr: "https://researchr.org/publication/icfp-1996"
  cites: 0
  citedby: 0
  booktitle: "Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), Philadelphia, Pennsylvania, May 24-26, 1996"
  conference: "ICFP"
  editor:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Richard L. Wexelblat"
    link: "https://researchr.org/alias/richard-l.-wexelblat"
  publisher: "ACM"
  isbn: "0-89791-770-7"
  kind: "proceedings"
  key: "icfp-1996"