@inproceedings{DreyerCH03,
  title = {A type system for higher-order modules},
  author = {Derek Dreyer and Karl Crary and Robert Harper},
  year = {2003},
  doi = {10.1145/640128.604151},
  url = {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},
}

@article{CavalloH21,
  title = {Internal Parametricity for Cubical Type Theory},
  author = {Evan Cavallo and Robert Harper},
  year = {2021},
  doi = {10.46298/lmcs-17(4:5)2021},
  url = {https://doi.org/10.46298/lmcs-17(4:5)2021},
  researchr = {https://researchr.org/publication/CavalloH21},
  cites = {0},
  citedby = {0},
  journal = {lmcs},
  volume = {17},
  number = {4},
}

@article{SterlingH21,
  title = {Logical Relations as Types: Proof-Relevant Parametricity for Program Modules},
  author = {Jonathan Sterling and Robert Harper},
  year = {2021},
  doi = {10.1145/3474834},
  url = {https://doi.org/10.1145/3474834},
  researchr = {https://researchr.org/publication/SterlingH21},
  cites = {0},
  citedby = {0},
  journal = {JACM},
  volume = {68},
  number = {6},
}

@inproceedings{MullerA017,
  title = {Responsive parallel computation: bridging competitive and cooperative threading},
  author = {Stefan K. Muller and Umut A. Acar and Robert Harper},
  year = {2017},
  doi = {10.1145/3062341.3062370},
  url = {http://doi.acm.org/10.1145/3062341.3062370},
  researchr = {https://researchr.org/publication/MullerA017},
  cites = {0},
  citedby = {0},
  pages = {677-692},
  booktitle = {PLDI},
}

@article{BlellochH15,
  title = {Cache efficient functional algorithms},
  author = {Guy E. Blelloch and Robert Harper},
  year = {2015},
  doi = {10.1145/2776825},
  url = {http://doi.acm.org/10.1145/2776825},
  researchr = {https://researchr.org/publication/BlellochH15},
  cites = {0},
  citedby = {0},
  journal = {CACM},
  volume = {58},
  number = {7},
  pages = {101-108},
}

@article{MorrisettH97,
  title = {Typed Closure Conversion for Recursively-Defined Functions},
  author = {J. Gregory Morrisett and Robert Harper},
  year = {1997},
  url = {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 = {ENTCS},
  volume = {10},
  pages = {230-241},
}

@inproceedings{HarperHP87,
  title = {A Framework for Defining Logics},
  author = {Robert Harper and Furio Honsell and Gordon D. Plotkin},
  year = {1987},
  tags = {logic},
  researchr = {https://researchr.org/publication/HarperHP87},
  cites = {0},
  citedby = {0},
  pages = {194-204},
  booktitle = {lics},
}

@inproceedings{HarperST89:0,
  title = {Structure and Representation in LF},
  author = {Robert Harper and Donald Sannella and Andrzej Tarlecki},
  year = {1989},
  researchr = {https://researchr.org/publication/HarperST89%3A0},
  cites = {0},
  citedby = {0},
  pages = {226-237},
  booktitle = {lics},
}

@article{AinsworthH07,
  title = {The PsyGrid Experience: Using Web Services in the Study of Schizophrenia},
  author = {John D. Ainsworth and Robert Harper},
  year = {2007},
  url = {http://www.igi-global.com/Bookstore/Article.aspx?TitleId=2201},
  tags = {web service, web services},
  researchr = {https://researchr.org/publication/AinsworthH07},
  cites = {0},
  citedby = {0},
  journal = {ijhisi},
  volume = {2},
  number = {2},
  pages = {1-20},
}

@inproceedings{SpoonhowerBHG08,
  title = {Space profiling for parallel functional programs},
  author = {Daniel Spoonhower and Guy E. Blelloch and Robert Harper and Phillip B. Gibbons},
  year = {2008},
  doi = {10.1145/1411204.1411240},
  url = {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 = {ICFP},
}

@article{Harper03:2,
  title = {Correcting computer-based assessments for guessing},
  author = {Robert Harper},
  year = {2003},
  doi = {10.1046/j.0266-4909.2002.00001.x},
  url = {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 = {jcal},
  volume = {19},
  number = {1},
  pages = {2-8},
}

@article{TassarottiH19,
  title = {A separation logic for concurrent randomized programs},
  author = {Joseph Tassarotti and Robert Harper},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290377},
  researchr = {https://researchr.org/publication/TassarottiH19},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {3},
}

@article{SalapuraHV13,
  title = {Resilient cloud computing},
  author = {Valentina Salapura and Robert Harper and M. Viswanathan},
  year = {2013},
  doi = {10.1147/JRD.2013.2266972},
  url = {http://dx.doi.org/10.1147/JRD.2013.2266972},
  researchr = {https://researchr.org/publication/SalapuraHV13},
  cites = {0},
  citedby = {0},
  journal = {ibmrd},
  volume = {57},
  number = {5},
}

@article{Harper94,
  title = {A Simplified Account of Polymorphic References},
  author = {Robert Harper},
  year = {1994},
  researchr = {https://researchr.org/publication/Harper94},
  cites = {0},
  citedby = {0},
  journal = {ipl},
  volume = {51},
  number = {4},
  pages = {201-206},
}

@article{Harper81,
  title = {PET and the IEEE 488 bus (GPIB): Eugene Fisher & Jensen, Osborne/McGraw-Hill (1980) 233 pp £10.00},
  author = {Robert Harper},
  year = {1981},
  doi = {10.1016/0141-9331(81)90529-9},
  url = {http://dx.doi.org/10.1016/0141-9331(81)90529-9},
  researchr = {https://researchr.org/publication/Harper81},
  cites = {0},
  citedby = {0},
  journal = {mam},
  volume = {5},
  number = {1},
  pages = {36-37},
}

@article{NanevskiBH03,
  title = {Automatic Generation of Staged Geometric Predicates},
  author = {Aleksandar Nanevski and Guy E. Blelloch and Robert Harper},
  year = {2003},
  doi = {10.1023/A:1025876920522},
  url = {http://dx.doi.org/10.1023/A:1025876920522},
  tags = {e-science},
  researchr = {https://researchr.org/publication/NanevskiBH03},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {16},
  number = {4},
  pages = {379-400},
}

@article{CraryH07,
  title = {Syntactic Logical Relations for Polymorphic and Recursive Types},
  author = {Karl Crary and Robert Harper},
  year = {2007},
  doi = {10.1016/j.entcs.2007.02.010},
  url = {http://dx.doi.org/10.1016/j.entcs.2007.02.010},
  researchr = {https://researchr.org/publication/CraryH07},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {172},
  pages = {259-299},
}

@book{0069232,
  title = {Definition of standard ML},
  author = {Robin Milner and Mads Tofte and Robert Harper},
  year = {1990},
  researchr = {https://researchr.org/publication/0069232},
  cites = {0},
  citedby = {0},
  publisher = {MIT Press},
  isbn = {978-0-262-63132-7},
}

@inproceedings{AcarBHVW04,
  title = {Dynamizing static algorithms, with applications to dynamic trees and history independence},
  author = {Umut A. Acar and Guy E. Blelloch and Robert Harper and Jorge L. Vittes and Shan Leung Maverick Woo},
  year = {2004},
  doi = {10.1145/982792.982871},
  url = {http://doi.acm.org/10.1145/982792.982871},
  tags = {history},
  researchr = {https://researchr.org/publication/AcarBHVW04},
  cites = {0},
  citedby = {0},
  pages = {531-540},
  booktitle = {soda},
}

@inproceedings{Harper09-0,
  title = {From tele ::::presence:::: to human ::::absence::::: the pragmatic construction of the human in communications systems research},
  author = {Robert Harper},
  year = {2009},
  doi = {10.1145/1671011.1671020},
  url = {http://doi.acm.org/10.1145/1671011.1671020},
  researchr = {https://researchr.org/publication/Harper09-0},
  cites = {0},
  citedby = {0},
  pages = {73-82},
  booktitle = {bcshci},
}

@inproceedings{MitchellH88,
  title = {The Essence of {ML}},
  author = {John C. Mitchell and Robert Harper},
  year = {1988},
  tags = {C++},
  researchr = {https://researchr.org/publication/MitchellH88},
  cites = {0},
  citedby = {0},
  pages = {28-46},
  booktitle = {POPL},
}

@article{AcarBBHT06,
  title = {A Library for Self-Adjusting Computation},
  author = {Umut A. Acar and Guy E. Blelloch and Matthias Blume and Robert Harper and Kanat Tangwongsan},
  year = {2006},
  doi = {10.1016/j.entcs.2005.11.043},
  url = {http://dx.doi.org/10.1016/j.entcs.2005.11.043},
  researchr = {https://researchr.org/publication/AcarBBHT06},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {148},
  number = {2},
  pages = {127-154},
}

@article{HarperP05,
  title = {On equivalence and canonical forms in the LF type theory},
  author = {Robert Harper and Frank Pfenning},
  year = {2005},
  doi = {10.1145/1042038.1042041},
  url = {http://doi.acm.org/10.1145/1042038.1042041},
  tags = {type theory},
  researchr = {https://researchr.org/publication/HarperP05},
  cites = {0},
  citedby = {0},
  journal = {tocl},
  volume = {6},
  number = {1},
  pages = {61-101},
}

@inproceedings{ProulxKH10,
  title = {Integrated visual analytics workflow with GeoTime and nSpace VAST 2010 mini challenge 1 award: Outstanding Analysis and Accuracy},
  author = {Pascale Proulx and Adeel Khamisa and Robert Harper},
  year = {2010},
  doi = {10.1109/VAST.2010.5653053},
  url = {http://dx.doi.org/10.1109/VAST.2010.5653053},
  tags = {analysis, workflow},
  researchr = {https://researchr.org/publication/ProulxKH10},
  cites = {0},
  citedby = {0},
  pages = {273-274},
  booktitle = {ieeevast},
}

@inproceedings{Cavallo020,
  title = {Internal Parametricity for Cubical Type Theory},
  author = {Evan Cavallo and Robert Harper},
  year = {2020},
  doi = {10.4230/LIPIcs.CSL.2020.13},
  url = {https://doi.org/10.4230/LIPIcs.CSL.2020.13},
  researchr = {https://researchr.org/publication/Cavallo020},
  cites = {0},
  citedby = {0},
  booktitle = {csl},
}

@article{Harper09,
  title = {FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum},
  author = {Robert Harper},
  year = {2009},
  doi = {10.1017/S0956796808007119},
  url = {http://dx.doi.org/10.1017/S0956796808007119},
  tags = {debugging},
  researchr = {https://researchr.org/publication/Harper09},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {19},
  number = {2},
  pages = {262},
}

@inproceedings{CraryHP99,
  title = {What is a Recursive Module?},
  author = {Karl Crary and Robert Harper and Sidd Puri},
  year = {1999},
  doi = {10.1145/301618.301641},
  url = {http://doi.acm.org/10.1145/301618.301641},
  researchr = {https://researchr.org/publication/CraryHP99},
  cites = {0},
  citedby = {0},
  pages = {50-63},
  booktitle = {PLDI},
}

@inproceedings{LeeCH07:0,
  title = {Towards a mechanized metatheory of standard ML},
  author = {Daniel K. Lee and Karl Crary and Robert Harper},
  year = {2007},
  doi = {10.1145/1190216.1190245},
  url = {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 = {POPL},
}

@inproceedings{DreyerHCK07,
  title = {Modular type classes},
  author = {Derek Dreyer and Robert Harper and Manuel M. T. Chakravarty and Gabriele Keller},
  year = {2007},
  doi = {10.1145/1190216.1190229},
  url = {http://doi.acm.org/10.1145/1190216.1190229},
  researchr = {https://researchr.org/publication/DreyerHCK07},
  cites = {0},
  citedby = {0},
  pages = {63-70},
  booktitle = {POPL},
}

@inproceedings{TarditiMCSHL96a,
  title = {TIL: a type-directed, optimizing compiler for ML (with retrospective)},
  author = {David Tarditi and J. Gregory Morrisett and Perry Cheng and Christopher A. Stone and Robert Harper and Peter Lee},
  year = {1996},
  doi = {10.1145/989393.989449},
  url = {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 = {PLDI},
}

@inproceedings{ChlipalaPH05,
  title = {Strict bidirectional type checking},
  author = {Adam J. Chlipala and Leaf Petersen and Robert Harper},
  year = {2005},
  doi = {10.1145/1040294.1040301},
  url = {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 = {tldi},
}

@inproceedings{AngiuliF018,
  title = {Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities},
  author = {Carlo Angiuli and Kuen-Bang Hou (Favonia) and Robert Harper},
  year = {2018},
  doi = {10.4230/LIPIcs.CSL.2018.6},
  url = {https://doi.org/10.4230/LIPIcs.CSL.2018.6},
  researchr = {https://researchr.org/publication/AngiuliF018},
  cites = {0},
  citedby = {0},
  booktitle = {csl},
}

@article{AngiuliBCHHL21,
  title = {Syntax and models of Cartesian cubical type theory},
  author = {Carlo Angiuli and Guillaume Brunerie and Thierry Coquand and Robert Harper and Kuen-Bang Hou (Favonia) and Daniel R. Licata},
  year = {2021},
  doi = {10.1017/S0960129521000347},
  url = {https://doi.org/10.1017/S0960129521000347},
  researchr = {https://researchr.org/publication/AngiuliBCHHL21},
  cites = {0},
  citedby = {0},
  journal = {mscs},
  volume = {31},
  number = {4},
  pages = {424-468},
}

@inproceedings{AcarBH03,
  title = {Selective memoization},
  author = {Umut A. Acar and Guy E. Blelloch and Robert Harper},
  year = {2003},
  doi = {10.1145/640128.604133},
  url = {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},
}

@article{AllenACFFGHHSWZ09,
  title = {An overview of the Oregon programming languages summer school},
  author = {Jim Allen and Zena M. Ariola and Pierre-Louis Curien and Matthew Fluet and Jeff Foster and Dan Grossman and Robert Harper and Hugo Herbelin and Yannis Smaragdakis and David Walker and Steve Zdancewic},
  year = {2009},
  doi = {10.1145/1816027.1816029},
  url = {http://doi.acm.org/10.1145/1816027.1816029},
  researchr = {https://researchr.org/publication/AllenACFFGHHSWZ09},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN},
  volume = {44},
  number = {11},
  pages = {1-3},
}

@inproceedings{Sterling022,
  title = {Sheaf Semantics of Termination-Insensitive Noninterference},
  author = {Jonathan Sterling and Robert Harper},
  year = {2022},
  doi = {10.4230/LIPIcs.FSCD.2022.5},
  url = {https://doi.org/10.4230/LIPIcs.FSCD.2022.5},
  researchr = {https://researchr.org/publication/Sterling022},
  cites = {0},
  citedby = {0},
  booktitle = {fscd},
}

@inproceedings{DonnellyHBFEFHM15,
  title = {Development and integration of a Surveillance Monitoring solution to provide earlier detection of the deteriorating patient},
  author = {N. Donnelly and Robert Harper and D. Branagh and J. Francey and H. Easlea and V. Faro-Maza and T. Hunniford and A. Mooney and J. McLaughlin},
  year = {2015},
  doi = {10.1109/EMBC.2015.7318581},
  url = {http://dx.doi.org/10.1109/EMBC.2015.7318581},
  researchr = {https://researchr.org/publication/DonnellyHBFEFHM15},
  cites = {0},
  citedby = {0},
  pages = {1198-1202},
  booktitle = {embc},
}

@inproceedings{AinsworthHJB06,
  title = {PsyGrid: Applying e-Science to Epidemiology},
  author = {John Ainsworth and Robert Harper and Ismael Juma and Iain E. Buchan},
  year = {2006},
  doi = {10.1109/CBMS.2006.135},
  url = {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 = {cbms},
}

@inproceedings{HarperJ04,
  title = {Self-adjusting beat detection and prediction in music},
  author = {Robert Harper and M. Ed Jernigan},
  year = {2004},
  doi = {10.1109/ICASSP.2004.1326809},
  url = {http://dx.doi.org/10.1109/ICASSP.2004.1326809},
  researchr = {https://researchr.org/publication/HarperJ04},
  cites = {0},
  citedby = {0},
  pages = {245-248},
  booktitle = {icassp},
}

@inproceedings{SwaseyVCH06,
  title = {A separate compilation extension to standard ML},
  author = {David Swasey and Tom Murphy VII and Karl Crary and Robert Harper},
  year = {2006},
  doi = {10.1145/1159876.1159883},
  url = {http://doi.acm.org/10.1145/1159876.1159883},
  researchr = {https://researchr.org/publication/SwaseyVCH06},
  cites = {0},
  citedby = {0},
  pages = {32-42},
  booktitle = {ml},
}

@article{HalpernHIKVV01,
  title = {On the unusual effectiveness of logic in computer science},
  author = {Joseph Y. Halpern and Robert Harper and Neil Immerman and Phokion G. Kolaitis and Moshe Y. Vardi and Victor Vianu},
  year = {2001},
  url = {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 = {bsl},
  volume = {7},
  number = {2},
  pages = {213-236},
}

@inproceedings{AcarBH02,
  title = {Adaptive functional programming},
  author = {Umut A. Acar and Guy E. Blelloch and Robert Harper},
  year = {2002},
  doi = {10.1145/503272.503296},
  url = {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},
}

@inproceedings{ProulxTBSHW06,
  title = {Avian Flu Case Study with nSpace and GeoTime},
  author = {Pascale Proulx and Sumeet Tandon and Adam Bodnar and David Schroh and Robert Harper and William Wright},
  year = {2006},
  doi = {10.1109/VAST.2006.261427},
  url = {http://dx.doi.org/10.1109/VAST.2006.261427},
  tags = {case study},
  researchr = {https://researchr.org/publication/ProulxTBSHW06},
  cites = {0},
  citedby = {0},
  pages = {27-34},
  booktitle = {ieeevast},
}

@book{Harper2012,
  title = {Practical Foundations for Programming Languages},
  author = {Robert Harper},
  year = {2012},
  tags = {programming languages},
  researchr = {https://researchr.org/publication/Harper2012},
  cites = {0},
  citedby = {0},
}

@inproceedings{SpoonhowerBH05,
  title = {Using page residency to balance tradeoffs in tracing garbage collection},
  author = {Daniel Spoonhower and Guy E. Blelloch and Robert Harper},
  year = {2005},
  doi = {10.1145/1064979.1064989},
  url = {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 = {vee},
}

@article{Harper08,
  title = {Position paper: practical foundations for lrogramming languages},
  author = {Robert Harper},
  year = {2008},
  doi = {10.1145/1480828.1480843},
  url = {http://doi.acm.org/10.1145/1480828.1480843},
  researchr = {https://researchr.org/publication/Harper08},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN},
  volume = {43},
  number = {11},
  pages = {71-73},
}

@inproceedings{HarperP91:0,
  title = {A Record Calculus Based on Symmetric Concatenation},
  author = {Robert Harper and Benjamin C. Pierce},
  year = {1991},
  tags = {rule-based, C++},
  researchr = {https://researchr.org/publication/HarperP91%3A0},
  cites = {0},
  citedby = {0},
  pages = {131-142},
  booktitle = {POPL},
}

@article{HarperP91,
  title = {Type Checking with Universes},
  author = {Robert Harper and Robert Pollack},
  year = {1991},
  tags = {type checking},
  researchr = {https://researchr.org/publication/HarperP91},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {89},
  number = {1},
  pages = {107-136},
}

@inproceedings{DubaHM91,
  title = {Typing First-Class Continuations in ML},
  author = {Bruce F. Duba and Robert Harper and David B. MacQueen},
  year = {1991},
  researchr = {https://researchr.org/publication/DubaHM91},
  cites = {0},
  citedby = {0},
  pages = {163-173},
  booktitle = {POPL},
}

@inproceedings{LicataZH08,
  title = {Focusing on Binding and Computation},
  author = {Daniel R. Licata and Noam Zeilberger and Robert Harper},
  year = {2008},
  doi = {10.1109/LICS.2008.48},
  url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48},
  researchr = {https://researchr.org/publication/LicataZH08},
  cites = {0},
  citedby = {0},
  pages = {241-252},
  booktitle = {lics},
}

@article{HouBH17,
  title = {Correctness of compiling polymorphism to dynamic typing},
  author = {Kuen-Bang Hou (Favonia) and Nick Benton and Robert Harper},
  year = {2017},
  doi = {10.1017/S0956796816000265},
  url = {http://dx.doi.org/10.1017/S0956796816000265},
  researchr = {https://researchr.org/publication/HouBH17},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {27},
}

@inproceedings{BernardHL98,
  title = {How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler},
  author = {Andrew Bernard and Robert Harper and Peter Lee},
  year = {1998},
  url = {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 = {tic},
}

@article{HarperL93:0,
  title = {Polymorphic Type Assignment and CPS Conversion},
  author = {Robert Harper and Mark Lillibridge},
  year = {1993},
  researchr = {https://researchr.org/publication/HarperL93%3A0},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {6},
  number = {3-4},
  pages = {361-380},
}

@article{HarperM96,
  title = {ML and Beyond},
  author = {Robert Harper and John C. Mitchell},
  year = {1996},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperM96},
  cites = {0},
  citedby = {0},
  journal = {ACM Comput. Surv.},
  volume = {28},
  number = {4es},
  pages = {219},
}

@inproceedings{MorrisettFH95,
  title = {Abstract Models of Memory Management},
  author = {J. Gregory Morrisett and Matthias Felleisen and Robert Harper},
  year = {1995},
  tags = {meta-model, memory management, Meta-Environment},
  researchr = {https://researchr.org/publication/MorrisettFH95},
  cites = {0},
  citedby = {0},
  pages = {66-77},
  booktitle = {fpca},
}

@inproceedings{EcclesKHW07,
  title = {Stories in GeoTime},
  author = {Ryan Eccles and Thomas Kapler and Robert Harper and William Wright},
  year = {2007},
  doi = {10.1109/VAST.2007.4388992},
  url = {http://dx.doi.org/10.1109/VAST.2007.4388992},
  researchr = {https://researchr.org/publication/EcclesKHW07},
  cites = {0},
  citedby = {0},
  pages = {19-26},
  booktitle = {ieeevast},
}

@inproceedings{KaplerEHW08,
  title = {Configurable Spaces: Temporal analysis in diagrammatic contexts},
  author = {Thomas Kapler and Ryan Eccles and Robert Harper and William Wright},
  year = {2008},
  doi = {10.1109/VAST.2008.4677355},
  url = {http://dx.doi.org/10.1109/VAST.2008.4677355},
  tags = {analysis, context-aware},
  researchr = {https://researchr.org/publication/KaplerEHW08},
  cites = {0},
  citedby = {0},
  pages = {43-50},
  booktitle = {ieeevast},
}

@article{Harper18,
  title = {Exception tracking in an open world},
  author = {Robert Harper},
  year = {2018},
  doi = {10.1016/j.tcs.2018.02.032},
  url = {https://doi.org/10.1016/j.tcs.2018.02.032},
  researchr = {https://researchr.org/publication/Harper18},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {741},
  pages = {25-31},
}

@inproceedings{BlellochH13,
  title = {Cache and I/O efficent functional algorithms},
  author = {Guy E. Blelloch and Robert Harper},
  year = {2013},
  doi = {10.1145/2429069.2429077},
  url = {http://doi.acm.org/10.1145/2429069.2429077},
  researchr = {https://researchr.org/publication/BlellochH13},
  cites = {0},
  citedby = {0},
  pages = {39-50},
  booktitle = {POPL},
}

@inproceedings{LicataH09,
  title = {A universe of binding and computation},
  author = {Daniel R. Licata and Robert Harper},
  year = {2009},
  doi = {10.1145/1596550.1596571},
  url = {http://doi.acm.org/10.1145/1596550.1596571},
  researchr = {https://researchr.org/publication/LicataH09},
  cites = {0},
  citedby = {0},
  pages = {123-134},
  booktitle = {ICFP},
}

@article{MandelbaumWH03-0,
  title = {An effective theory of type refinements},
  author = {Yitzhak Mandelbaum and David Walker and Robert Harper},
  year = {2003},
  doi = {10.1145/944746.944725},
  url = {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},
  volume = {38},
  number = {9},
  pages = {213-225},
}

@article{ProulxCHSKJW07,
  title = {nSpace and GeoTime: A VAST 2006 Case Study},
  author = {Pascale Proulx and Lynn Chien and Robert Harper and David Schroh and Thomas Kapler and David Jonker and William Wright},
  year = {2007},
  doi = {10.1109/MCG.2007.131},
  url = {http://doi.ieeecomputersociety.org/10.1109/MCG.2007.131},
  tags = {case study},
  researchr = {https://researchr.org/publication/ProulxCHSKJW07},
  cites = {0},
  citedby = {0},
  journal = {cga},
  volume = {27},
  number = {5},
  pages = {46-56},
}

@article{Harper99:0,
  title = {Proof-Directed Debugging},
  author = {Robert Harper},
  year = {1999},
  tags = {debugging},
  researchr = {https://researchr.org/publication/Harper99%3A0},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {9},
  number = {4},
  pages = {463-469},
}

@inproceedings{HarperMM90,
  title = {Higher-Order Modules and the Phase Distinction},
  author = {Robert Harper and John C. Mitchell and Eugenio Moggi},
  year = {1990},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperMM90},
  cites = {0},
  citedby = {0},
  pages = {341-354},
  booktitle = {POPL},
}

@inproceedings{BaileyBFHR09,
  title = {Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report},
  author = {Mark W. Bailey and Kim B. Bruce and Kathleen Fisher and Robert Harper and Stuart Reges},
  year = {2009},
  doi = {10.1145/1508865.1508913},
  url = {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 = {sigcse},
}

@inproceedings{VIICHP04,
  title = {A Symmetric Modal Lambda Calculus for Distributed Computing},
  author = {Tom Murphy VII and Karl Crary and Robert Harper and Frank Pfenning},
  year = {2004},
  url = {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 = {lics},
}

@article{HarperDM93,
  title = {Typing First-Class Continuations in ML},
  author = {Robert Harper and Bruce F. Duba and David B. MacQueen},
  year = {1993},
  researchr = {https://researchr.org/publication/HarperDM93},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {3},
  number = {4},
  pages = {465-484},
}

@inproceedings{ConstantinescuPHM08,
  title = {Silent Data Corruption - Myth or reality?},
  author = {Cristian Constantinescu and Ishwar Parulkar and Robert Harper and Sarah Michalak},
  year = {2008},
  doi = {10.1109/DSN.2008.4630077},
  url = {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 = {dsn},
}

@inproceedings{MandelbaumWH03,
  title = {An effective theory of type refinements},
  author = {Yitzhak Mandelbaum and David Walker and Robert Harper},
  year = {2003},
  doi = {10.1145/944705.944725},
  url = {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 = {ICFP},
}

@article{LicataH11,
  title = {2-Dimensional Directed Type Theory},
  author = {Daniel R. Licata and Robert Harper},
  year = {2011},
  doi = {10.1016/j.entcs.2011.09.026},
  url = {http://dx.doi.org/10.1016/j.entcs.2011.09.026},
  researchr = {https://researchr.org/publication/LicataH11},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {276},
  pages = {263-289},
}

@inproceedings{AinsworthHJB06-0,
  title = {Design and implementation of security in a data collection system for epidemiology},
  author = {John D. Ainsworth and Robert Harper and Ismael Juma and Iain E. Buchan},
  year = {2006},
  url = {http://www.booksonline.iospress.nl/Content/View.aspx?piid=4754},
  researchr = {https://researchr.org/publication/AinsworthHJB06-0},
  cites = {0},
  citedby = {0},
  pages = {348-357},
  booktitle = {healthgrid},
}

@article{MullerA018,
  title = {Competitive parallelism: getting your priorities right},
  author = {Stefan K. Muller and Umut A. Acar and Robert Harper},
  year = {2018},
  doi = {10.1145/3236790},
  url = {https://doi.org/10.1145/3236790},
  researchr = {https://researchr.org/publication/MullerA018},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {2},
  number = {ICFP},
}

@inproceedings{PetersenHCP03,
  title = {A type theory for memory allocation and data layout},
  author = {Leaf Petersen and Robert Harper and Karl Crary and Frank Pfenning},
  year = {2003},
  doi = {10.1145/640128.604147},
  url = {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},
}

@article{HarperL96,
  title = {Research in Programming Languages for Composability, Safety, and Performance},
  author = {Robert Harper and Peter Lee},
  year = {1996},
  tags = {programming languages, programming},
  researchr = {https://researchr.org/publication/HarperL96},
  cites = {0},
  citedby = {0},
  journal = {ACM Comput. Surv.},
  volume = {28},
  number = {4es},
  pages = {195},
}

@inproceedings{NanevskiBH01,
  title = {Automatic Generation of Staged Geometric Predicates},
  author = {Aleksandar Nanevski and Guy E. Blelloch and Robert Harper},
  year = {2001},
  tags = {e-science},
  researchr = {https://researchr.org/publication/NanevskiBH01},
  cites = {0},
  citedby = {0},
  pages = {217-228},
  booktitle = {ICFP},
}

@article{AcarBH06,
  title = {Adaptive functional programming},
  author = {Umut A. Acar and Guy E. Blelloch and Robert Harper},
  year = {2006},
  doi = {10.1145/1186634},
  url = {http://doi.acm.org/10.1145/1186634},
  tags = {functional programming, e-science, programming},
  researchr = {https://researchr.org/publication/AcarBH06},
  cites = {0},
  citedby = {0},
  journal = {TOPLAS},
  volume = {28},
  number = {6},
  pages = {990-1034},
}

@article{EcclesKHW08,
  title = {Stories in GeoTime},
  author = {Ryan Eccles and Thomas Kapler and Robert Harper and William Wright},
  year = {2008},
  doi = {10.1057/palgrave.ivs.9500173},
  url = {http://dx.doi.org/10.1057/palgrave.ivs.9500173},
  researchr = {https://researchr.org/publication/EcclesKHW08},
  cites = {0},
  citedby = {0},
  journal = {ivs},
  volume = {7},
  number = {1},
  pages = {3-17},
}

@inproceedings{TassarottiJ017,
  title = {A Higher-Order Logic for Concurrent Termination-Preserving Refinement},
  author = {Joseph Tassarotti and Ralf Jung and Robert Harper},
  year = {2017},
  doi = {10.1007/978-3-662-54434-1_34},
  url = {http://dx.doi.org/10.1007/978-3-662-54434-1_34},
  researchr = {https://researchr.org/publication/TassarottiJ017},
  cites = {0},
  citedby = {0},
  pages = {909-936},
  booktitle = {ESOP},
}

@article{BiagioniHL01,
  title = {A Network Protocol Stack in Standard ML},
  author = {Edoardo Biagioni and Robert Harper and Peter Lee},
  year = {2001},
  tags = {protocol},
  researchr = {https://researchr.org/publication/BiagioniHL01},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {14},
  number = {4},
  pages = {309-356},
}

@article{HarperM97,
  title = {ML and Beyond},
  author = {Robert Harper and John C. Mitchell},
  year = {1997},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperM97},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN},
  volume = {32},
  number = {1},
  pages = {80-85},
}

@inproceedings{VIICH05,
  title = {Distributed Control Flow with Classical Modal Logic},
  author = {Tom Murphy VII and Karl Crary and Robert Harper},
  year = {2005},
  doi = {10.1007/11538363_6},
  url = {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 = {csl},
}

@inproceedings{AvijitDH10,
  title = {Distributed programming with distributed authorization},
  author = {Kumar Avijit and Anupam Datta and Robert Harper},
  year = {2010},
  doi = {10.1145/1708016.1708021},
  url = {http://doi.acm.org/10.1145/1708016.1708021},
  tags = {programming},
  researchr = {https://researchr.org/publication/AvijitDH10},
  cites = {0},
  citedby = {0},
  pages = {27-38},
  booktitle = {tldi},
}

@inproceedings{VanderwaartDPCHC03,
  title = {Typed compilation of recursive datatypes},
  author = {Joseph Vanderwaart and Derek Dreyer and Leaf Petersen and Karl Crary and Robert Harper and Perry Cheng},
  year = {2003},
  doi = {10.1145/604174.604187},
  url = {http://doi.acm.org/10.1145/604174.604187},
  researchr = {https://researchr.org/publication/VanderwaartDPCHC03},
  cites = {0},
  citedby = {0},
  pages = {98-108},
  booktitle = {tldi},
}

@phdthesis{us-153,
  title = {Aspects of the Implementation of Type Theory},
  author = {Robert Harper},
  year = {1985},
  researchr = {https://researchr.org/publication/us-153},
  cites = {0},
  citedby = {0},
  school = {Cornell University, USA},
}

@article{Harper96,
  title = {A Note on   A Simplified Account of Polymorphic References  },
  author = {Robert Harper},
  year = {1996},
  doi = {10.1016/0020-0190(95)00178-6},
  url = {http://dx.doi.org/10.1016/0020-0190(95)00178-6},
  researchr = {https://researchr.org/publication/Harper96},
  cites = {0},
  citedby = {0},
  journal = {ipl},
  volume = {57},
  number = {1},
  pages = {15-16},
}

@inproceedings{ChangCDHLVP02,
  title = {Trustless Grid Computing in ConCert},
  author = {Bor-Yuh Evan Chang and Karl Crary and Margaret DeLap and Robert Harper and Jason Liszka and Tom Murphy VII and Frank Pfenning},
  year = {2002},
  url = {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 = {ccgrid},
}

@article{HarperP98,
  title = {A Module System for a Programming Language Based on the LF Logical Framework},
  author = {Robert Harper and Frank Pfenning},
  year = {1998},
  tags = {programming languages, rule-based, programming},
  researchr = {https://researchr.org/publication/HarperP98},
  cites = {0},
  citedby = {0},
  journal = {logcom},
  volume = {8},
  number = {1},
  pages = {5-31},
}

@article{HarperHP93,
  title = {A Framework for Defining Logics},
  author = {Robert Harper and Furio Honsell and Gordon D. Plotkin},
  year = {1993},
  doi = {10.1145/138027.138060},
  url = {http://doi.acm.org/10.1145/138027.138060},
  tags = {logic},
  researchr = {https://researchr.org/publication/HarperHP93},
  cites = {0},
  citedby = {0},
  journal = {JACM},
  volume = {40},
  number = {1},
  pages = {143-184},
}

@article{HarperM93,
  title = {On the Type Structure of Standard ML},
  author = {Robert Harper and John C. Mitchell},
  year = {1993},
  doi = {10.1145/169701.169696},
  url = {http://doi.acm.org/10.1145/169701.169696},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperM93},
  cites = {0},
  citedby = {0},
  journal = {TOPLAS},
  volume = {15},
  number = {2},
  pages = {211-252},
}

@inproceedings{TarditiMCSHL96,
  title = {TIL: A Type-Directed Optimizing Compiler for ML},
  author = {David Tarditi and J. Gregory Morrisett and Perry Cheng and Christopher A. Stone and Robert Harper and Peter Lee},
  year = {1996},
  tags = {optimization, compiler},
  researchr = {https://researchr.org/publication/TarditiMCSHL96},
  cites = {0},
  citedby = {0},
  pages = {181-192},
  booktitle = {PLDI},
}

@inproceedings{BirkedalH97,
  title = {Relational Interpretations of Recursive Types in an operational Setting (Summary)},
  author = {Lars Birkedal and Robert Harper},
  year = {1997},
  researchr = {https://researchr.org/publication/BirkedalH97},
  cites = {0},
  citedby = {0},
  pages = {458-490},
  booktitle = {tacs},
}

@inproceedings{HarperST89,
  title = {Logic Representation in LF},
  author = {Robert Harper and Donald Sannella and Andrzej Tarlecki},
  year = {1989},
  tags = {logic},
  researchr = {https://researchr.org/publication/HarperST89},
  cites = {0},
  citedby = {0},
  pages = {250-272},
  booktitle = {ctcs},
}

@inproceedings{MinamideMH96,
  title = {Typed Closure Conversion},
  author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper},
  year = {1996},
  doi = {10.1145/237721.237791},
  url = {http://doi.acm.org/10.1145/237721.237791},
  researchr = {https://researchr.org/publication/MinamideMH96},
  cites = {0},
  citedby = {0},
  pages = {271-283},
  booktitle = {POPL},
}

@inproceedings{Harper05:0,
  title = {Mechanizing the meta-theory of programming languages},
  author = {Robert Harper},
  year = {2005},
  doi = {10.1145/1086365.1086396},
  url = {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 = {ICFP},
}

@article{Harper83,
  title = {Microprocessor-based multichannel analyser developed using POLYFORTH},
  author = {Robert Harper},
  year = {1983},
  doi = {10.1016/0141-9331(83)90328-9},
  url = {http://dx.doi.org/10.1016/0141-9331(83)90328-9},
  researchr = {https://researchr.org/publication/Harper83},
  cites = {0},
  citedby = {0},
  journal = {mam},
  volume = {7},
  number = {5},
  pages = {217-222},
}

@inproceedings{SpoonhowerBGH09,
  title = {Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures},
  author = {Daniel Spoonhower and Guy E. Blelloch and Phillip B. Gibbons and Robert Harper},
  year = {2009},
  doi = {10.1145/1583991.1584019},
  url = {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},
}

@article{CavalloH19,
  title = {Higher inductive types in cubical computational type theory},
  author = {Evan Cavallo and Robert Harper},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290314},
  researchr = {https://researchr.org/publication/CavalloH19},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {3},
}

@inproceedings{Harper04:0,
  title = {Self-Adjusting Computation},
  author = {Robert Harper},
  year = {2004},
  url = {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 = {lics},
}

@inproceedings{ChenDSWHB06,
  title = {Consolidating clients on back-end servers with co-location and frequency control},
  author = {Yiyu Chen and Amitayu Das and Anand Sivasubramaniam and Qian Wang and Robert Harper and M. Bland},
  year = {2006},
  doi = {10.1145/1140277.1140331},
  url = {http://doi.acm.org/10.1145/1140277.1140331},
  researchr = {https://researchr.org/publication/ChenDSWHB06},
  cites = {0},
  citedby = {0},
  pages = {383-384},
  booktitle = {sigmetrics},
}

@inproceedings{LicataH09-0,
  title = {Positively dependent types},
  author = {Daniel R. Licata and Robert Harper},
  year = {2009},
  doi = {10.1145/1481848.1481851},
  url = {http://doi.acm.org/10.1145/1481848.1481851},
  researchr = {https://researchr.org/publication/LicataH09-0},
  cites = {0},
  citedby = {0},
  pages = {3-14},
  booktitle = {plpv},
}

@inproceedings{HarperRSEHM08,
  title = {The past is a different place: they do things differently there},
  author = {Robert Harper and D. Randall and N. Smyth and C. Evans and L. Heledd and R. Moore},
  year = {2008},
  doi = {10.1145/1394445.1394474},
  url = {http://doi.acm.org/10.1145/1394445.1394474},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperRSEHM08},
  cites = {0},
  citedby = {0},
  pages = {271-280},
  booktitle = {ACMdis},
}

@article{SpoonhowerBHG08-0,
  title = {Space profiling for parallel functional programs},
  author = {Daniel Spoonhower and Guy E. Blelloch and Robert Harper and Phillip B. Gibbons},
  year = {2008},
  doi = {10.1017/S0956796810000146},
  url = {http://dx.doi.org/10.1017/S0956796810000146},
  tags = {functional programming, parallel programming, e-science},
  researchr = {https://researchr.org/publication/SpoonhowerBHG08-0},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {20},
  number = {5-6},
  pages = {417-461},
}

@inproceedings{HarperP89,
  title = {Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft)},
  author = {Robert Harper and Robert Pollack},
  year = {1989},
  tags = {type checking},
  researchr = {https://researchr.org/publication/HarperP89},
  cites = {0},
  citedby = {0},
  pages = {241-256},
  booktitle = {tapsoft},
}

@inproceedings{HarperP00,
  title = {Advanced module systems: a guide for the perplexed (abstract of invited talk)},
  author = {Robert Harper and Benjamin C. Pierce},
  year = {2000},
  doi = {10.1145/351240.351252},
  url = {http://doi.acm.org/10.1145/351240.351252},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperP00},
  cites = {0},
  citedby = {0},
  pages = {130},
  booktitle = {ICFP},
}

@inproceedings{SchneiderMH01,
  title = {A Language-Based Approach to Security},
  author = {Fred B. Schneider and J. Gregory Morrisett and Robert Harper},
  year = {2001},
  url = {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 = {Dagstuhl},
}

@article{AngiuliMLH16,
  title = {Homotopical patch theory},
  author = {Carlo Angiuli and Edward Morehouse and Daniel R. Licata and Robert Harper},
  year = {2016},
  doi = {10.1017/S0956796816000198},
  url = {http://dx.doi.org/10.1017/S0956796816000198},
  researchr = {https://researchr.org/publication/AngiuliMLH16},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {26},
}

@article{NiuSGH22,
  title = {A cost-aware logical framework},
  author = {Yue Niu and Jonathan Sterling and Harrison Grodin and Robert Harper},
  year = {2022},
  doi = {10.1145/3498670},
  url = {https://doi.org/10.1145/3498670},
  researchr = {https://researchr.org/publication/NiuSGH22},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {6},
  number = {POPL},
  pages = {1-31},
}

@article{AwodeyH15,
  title = {Homotopy type theory: unified foundations of mathematics and computation},
  author = {Steve Awodey and Robert Harper},
  year = {2015},
  doi = {10.1145/2728816.2728825},
  url = {http://doi.acm.org/10.1145/2728816.2728825},
  researchr = {https://researchr.org/publication/AwodeyH15},
  cites = {0},
  citedby = {0},
  journal = {siglog},
  volume = {2},
  number = {1},
  pages = {37-44},
}

@inproceedings{HarperM95,
  title = {Compiling Polymorphism Using Intensional Type Analysis},
  author = {Robert Harper and J. Gregory Morrisett},
  year = {1995},
  tags = {analysis, compiler},
  researchr = {https://researchr.org/publication/HarperM95},
  cites = {0},
  citedby = {0},
  pages = {130-141},
  booktitle = {POPL},
}

@article{AllenBBBFFHKKLLLPRRSTW08,
  title = {SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations},
  author = {Eric Allen and Mark W. Bailey and Rastislav Bodík and Kim B. Bruce and Kathleen Fisher and Stephen N. Freund and Robert Harper and Chandra Krintz and Shriram Krishnamurthi and James R. Larus and Doug Lea and Gary T. Leavens and Lori L. Pollock and Stuart Reges and Martin C. Rinard and Mark Sheldon and Franklyn A. Turbak and Mitchell Wand},
  year = {2008},
  doi = {10.1145/1480828.1480831},
  url = {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},
  volume = {43},
  number = {11},
  pages = {6-29},
}

@article{BasinDH04,
  title = {Editorial},
  author = {David A. Basin and Olivier Danvy and Robert Harper},
  year = {2004},
  doi = {10.1023/B:LISP.0000029480.20108.7d},
  url = {http://dx.doi.org/10.1023/B:LISP.0000029480.20108.7d},
  researchr = {https://researchr.org/publication/BasinDH04},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {17},
  number = {3},
  pages = {171},
}

@inproceedings{Tassarotti018,
  title = {Verified Tail Bounds for Randomized Programs},
  author = {Joseph Tassarotti and Robert Harper},
  year = {2018},
  doi = {10.1007/978-3-319-94821-8_33},
  url = {https://doi.org/10.1007/978-3-319-94821-8_33},
  researchr = {https://researchr.org/publication/Tassarotti018},
  cites = {0},
  citedby = {0},
  pages = {560-578},
  booktitle = {itp},
}

@book{Milner1997thedefinition,
  title = {The Definition of {S}tandard {ML}, Revised},
  author = {Milner, Robin and Tofte, Mads and Robert Harper and MacQueen, David},
  year = {1997},
  researchr = {https://researchr.org/publication/Milner1997thedefinition},
  cites = {0},
  citedby = {0},
  address = {Cambridge, MA, USA},
  publisher = {MIT Press},
}

@inproceedings{HarperLZ09,
  title = {A Pronominal Approach to Binding and Computation},
  author = {Robert Harper and Daniel R. Licata and Noam Zeilberger},
  year = {2009},
  doi = {10.1007/978-3-642-02273-9_2},
  url = {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 = {tlca},
}

@article{ColbyCHLP03,
  title = {Automated techniques for provably safe mobile code},
  author = {Christopher Colby and Karl Crary and Robert Harper and Peter Lee and Frank Pfenning},
  year = {2003},
  tags = {mobile code, mobile},
  researchr = {https://researchr.org/publication/ColbyCHLP03},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {290},
  number = {2},
  pages = {1175-1199},
}

@inproceedings{XiH01,
  title = {A Dependently Typed Assembly Language},
  author = {Hongwei Xi and Robert Harper},
  year = {2001},
  researchr = {https://researchr.org/publication/XiH01},
  cites = {0},
  citedby = {0},
  pages = {169-180},
  booktitle = {ICFP},
}

@article{HarperST94,
  title = {Structured Theory Presentations and Logic Representations},
  author = {Robert Harper and Donald Sannella and Andrzej Tarlecki},
  year = {1994},
  tags = {logic},
  researchr = {https://researchr.org/publication/HarperST94},
  cites = {0},
  citedby = {0},
  journal = {APAL},
  volume = {67},
  number = {1-3},
  pages = {113-160},
}

@inproceedings{Harper04,
  title = {Self-Adjusting Computation},
  author = {Robert Harper},
  year = {2004},
  url = {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 = {icalp},
}

@inproceedings{VIICH07,
  title = {Type-Safe Distributed Programming with ML5},
  author = {Tom Murphy VII and Karl Crary and Robert Harper},
  year = {2007},
  doi = {10.1007/978-3-540-78663-4_9},
  url = {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 = {tgc},
}

@article{BirkedalH99,
  title = {Relational Interpretations of Recursive Types in an Operational Setting},
  author = {Lars Birkedal and Robert Harper},
  year = {1999},
  researchr = {https://researchr.org/publication/BirkedalH99},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {155},
  number = {1-2},
  pages = {3-63},
}

@inproceedings{Harper85,
  title = {Modules and Persistence in Standard ML},
  author = {Robert Harper},
  year = {1985},
  researchr = {https://researchr.org/publication/Harper85},
  cites = {0},
  citedby = {0},
  pages = {21-30},
  booktitle = {pos},
}

@inproceedings{LicataH12,
  title = {Canonicity for 2-dimensional type theory},
  author = {Daniel R. Licata and Robert Harper},
  year = {2012},
  doi = {10.1145/2103656.2103697},
  url = {http://doi.acm.org/10.1145/2103656.2103697},
  researchr = {https://researchr.org/publication/LicataH12},
  cites = {0},
  citedby = {0},
  pages = {337-348},
  booktitle = {POPL},
}

@article{Harper92,
  title = {Constructing Type Systems over an Operational Semantics},
  author = {Robert Harper},
  year = {1992},
  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 = {JSC},
  volume = {14},
  number = {1},
  pages = {71-84},
}

@article{BlellochBCHMW01,
  title = {Persistent triangulations Journal of Functional Programming},
  author = {Guy E. Blelloch and Hal Burch and Karl Crary and Robert Harper and Gary L. Miller and Noel Walkington},
  year = {2001},
  tags = {persistent, functional programming, programming},
  researchr = {https://researchr.org/publication/BlellochBCHMW01},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {11},
  number = {5},
  pages = {441-466},
}

@inproceedings{AngiuliMLH14,
  title = {Homotopical patch theory},
  author = {Carlo Angiuli and Edward Morehouse and Daniel R. Licata and Robert Harper},
  year = {2014},
  doi = {10.1145/2628136.2628158},
  url = {http://doi.acm.org/10.1145/2628136.2628158},
  researchr = {https://researchr.org/publication/AngiuliMLH14},
  cites = {0},
  citedby = {0},
  pages = {243-256},
  booktitle = {ICFP},
}

@inproceedings{BiagioniHLM94,
  title = {Signatures for a Network Protocol Stack: A Systems Application of Standard ML},
  author = {Edoardo Biagioni and Robert Harper and Peter Lee and Brian Milnes},
  year = {1994},
  doi = {10.1145/182409.182431},
  url = {http://doi.acm.org/10.1145/182409.182431},
  tags = {protocol},
  researchr = {https://researchr.org/publication/BiagioniHLM94},
  cites = {0},
  citedby = {0},
  pages = {55-64},
  booktitle = {lfp},
}

@article{HarperL96:0,
  title = {Operational Interpretations of an Extension of F::omega:: with Control Operators},
  author = {Robert Harper and Mark Lillibridge},
  year = {1996},
  researchr = {https://researchr.org/publication/HarperL96%3A0},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {6},
  number = {3},
  pages = {393-417},
}

@inproceedings{GordonHHJS11,
  title = {Robin Milner 1934--2010: verification, languages, and concurrency},
  author = {Andrew D. Gordon and Robert Harper and John Harrison and Alan Jeffrey and Peter Sewell},
  year = {2011},
  doi = {10.1145/1926385.1926439},
  url = {http://doi.acm.org/10.1145/1926385.1926439},
  researchr = {https://researchr.org/publication/GordonHHJS11},
  cites = {0},
  citedby = {0},
  pages = {473-474},
  booktitle = {POPL},
}

@inproceedings{HarperL94,
  title = {A Type-Theoretic Approach to Higher-Order Modules with Sharing},
  author = {Robert Harper and Mark Lillibridge},
  year = {1994},
  tags = {systematic-approach},
  researchr = {https://researchr.org/publication/HarperL94},
  cites = {0},
  citedby = {0},
  pages = {123-137},
  booktitle = {POPL},
}

@article{HarperM99,
  title = {Parametricity and Variants of Girard s ::::J:::: Operator},
  author = {Robert Harper and John C. Mitchell},
  year = {1999},
  doi = {10.1016/S0020-0190(99)00036-8},
  url = {http://dx.doi.org/10.1016/S0020-0190(99)00036-8},
  tags = {C++},
  researchr = {https://researchr.org/publication/HarperM99},
  cites = {0},
  citedby = {0},
  journal = {ipl},
  volume = {70},
  number = {1},
  pages = {1-5},
}

@inproceedings{StoneH00,
  title = {Deciding Type Equivalence with Singleton Kinds},
  author = {Christopher A. Stone and Robert Harper},
  year = {2000},
  doi = {10.1145/325694.325724},
  url = {http://doi.acm.org/10.1145/325694.325724},
  researchr = {https://researchr.org/publication/StoneH00},
  cites = {0},
  citedby = {0},
  pages = {214-227},
  booktitle = {POPL},
}

@inproceedings{HarperS00,
  title = {A type-theoretic interpretation of standard ML},
  author = {Robert Harper and Christopher A. Stone},
  year = {2000},
  researchr = {https://researchr.org/publication/HarperS00},
  cites = {0},
  citedby = {0},
  pages = {341-388},
  booktitle = {BIRTHDAY},
}

@inproceedings{HarperMT87,
  title = {A Type Discipline for Program Modules},
  author = {Robert Harper and Robin Milner and Mads Tofte},
  year = {1987},
  researchr = {https://researchr.org/publication/HarperMT87},
  cites = {0},
  citedby = {0},
  pages = {308-319},
  booktitle = {tapsoft},
}

@article{AcarBBHT09,
  title = {An experimental analysis of self-adjusting computation},
  author = {Umut A. Acar and Guy E. Blelloch and Matthias Blume and Robert Harper and Kanat Tangwongsan},
  year = {2009},
  doi = {10.1145/1596527.1596530},
  url = {http://doi.acm.org/10.1145/1596527.1596530},
  tags = {analysis},
  researchr = {https://researchr.org/publication/AcarBBHT09},
  cites = {0},
  citedby = {0},
  journal = {TOPLAS},
  volume = {32},
  number = {1},
}

@inproceedings{HarperL93,
  title = {Explicit Polymorphism and CPS Conversion},
  author = {Robert Harper and Mark Lillibridge},
  year = {1993},
  researchr = {https://researchr.org/publication/HarperL93},
  cites = {0},
  citedby = {0},
  pages = {206-219},
  booktitle = {POPL},
}

@inproceedings{ChengHL98,
  title = {Generational Stack Collection and Profile-Driven Pretenuring},
  author = {Perry Cheng and Robert Harper and Peter Lee},
  year = {1998},
  researchr = {https://researchr.org/publication/ChengHL98},
  cites = {0},
  citedby = {0},
  pages = {162-173},
  booktitle = {PLDI},
}

@article{HarperL07,
  title = {Mechanizing metatheory in a logical framework},
  author = {Robert Harper and Daniel R. Licata},
  year = {2007},
  doi = {10.1017/S0956796807006430},
  url = {http://dx.doi.org/10.1017/S0956796807006430},
  tags = {metatheory},
  researchr = {https://researchr.org/publication/HarperL07},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {17},
  number = {4-5},
  pages = {613-673},
}

@article{CraryH06,
  title = {Higher-order abstract syntax: setting the record straight},
  author = {Karl Crary and Robert Harper},
  year = {2006},
  doi = {10.1145/1165555.1165572},
  url = {http://doi.acm.org/10.1145/1165555.1165572},
  tags = {abstract syntax},
  researchr = {https://researchr.org/publication/CraryH06},
  cites = {0},
  citedby = {0},
  journal = {sigact},
  volume = {37},
  number = {3},
  pages = {93-96},
}

@article{StoneH06,
  title = {Extensional equivalence and singleton types},
  author = {Christopher A. Stone and Robert Harper},
  year = {2006},
  doi = {10.1145/1183278.1183281},
  url = {http://doi.acm.org/10.1145/1183278.1183281},
  researchr = {https://researchr.org/publication/StoneH06},
  cites = {0},
  citedby = {0},
  journal = {tocl},
  volume = {7},
  number = {4},
  pages = {676-722},
}
@proceedings{tic:2000,
  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 = {Robert Harper},
  volume = {2071},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-42196-3},
}

@proceedings{icfp-1996,
  title = {Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), Philadelphia, Pennsylvania, May 24-26, 1996},
  year = {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 = {Robert Harper and Richard L. Wexelblat},
  publisher = {ACM},
  isbn = {0-89791-770-7},
}