@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 = {Logical Methods in Computer Science}, 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 = {Journal of the ACM}, 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 = {Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017}, editor = {Albert Cohen 0001 and Martin T. Vechev}, publisher = {ACM}, isbn = {978-1-4503-4988-8}, } @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 = {Communications of the ACM}, 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 = {Electronic Notes in Theoretical Computer Science}, 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 = {Proceedings, Symposium on Logic in Computer Science, 22-25 June 1987, Ithaca, New York, USA}, publisher = {IEEE Computer Society}, } @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 = {Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA}, publisher = {IEEE Computer Society}, } @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 = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008}, editor = {James Hook and Peter Thiemann}, publisher = {ACM}, isbn = {978-1-59593-919-7}, } @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 = {J. Comp. Assisted Learning}, 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 = {Proceedings of the ACM on Programming Languages}, 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 = {IBM Journal of Research and Development}, 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 = {Inf. Process. Lett.}, 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 = {Microprocessors and Microsystems}, 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 = {Higher-Order and Symbolic Computation}, 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 = {Electronic Notes in Theoretical Computer Science}, 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 = {Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004}, editor = {J. Ian Munro}, publisher = {SIAM}, } @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 = {Proceedings of the 2009 British Computer Society Conference on Human-Computer Interaction, BCS-HCI 2009, Cambridge, United Kingdom, 1-5 September 2009}, publisher = {ACM}, } @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 = {Electronic Notes in Theoretical Computer Science}, 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 = {ACM Trans. Comput. Log.}, 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 = {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}, } @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 = {28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain}, editor = {Maribel Fernández and Anca Muscholl}, volume = {152}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, isbn = {978-3-95977-132-0}, } @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 = {Journal of Functional Programming}, 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 = {Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007}, editor = {Martin Hofmann and Matthias Felleisen}, publisher = {ACM}, isbn = {1-59593-575-4}, } @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 = {Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007}, editor = {Martin Hofmann and Matthias Felleisen}, publisher = {ACM}, isbn = {1-59593-575-4}, } @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 = {20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection}, editor = {Kathryn S. McKinley}, publisher = {ACM}, isbn = {1-58113-623-4}, } @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 = {Proceedings of TLDI 05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Long Beach, CA, USA, January 10, 2005}, editor = {J. Gregory Morrisett and Manuel Fähndrich}, publisher = {ACM}, isbn = {1-58113-999-3}, } @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 = {27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK}, editor = {Dan R. Ghica and Achim Jung}, volume = {119}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, isbn = {978-3-95977-088-0}, } @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 = {Mathematical Structures in Computer Science}, 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 Notices}, 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 = {7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel}, editor = {Amy P. Felty}, volume = {228}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, isbn = {978-3-95977-233-4}, } @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 = {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}, } @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 = {19th IEEE International Symposium on Computer-Based Medical Systems (CBMS 2006), 22-23 June 2006, Salt Lake City, Utah, USA}, publisher = {IEEE Computer Society}, } @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 = {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}, } @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 = {Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006}, editor = {Andrew Kennedy and François Pottier}, publisher = {ACM}, isbn = {1-59593-483-9}, } @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 = {Bulletin of Symbolic Logic}, 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 = {IEEE Symposium On Visual Analytics Science And Technology, IEEE VAST 2006, October 31-November 2, 2006, Baltimore, Maryland, USA}, editor = {Pak Chung Wong and Daniel A. Keim}, publisher = {IEEE}, isbn = {1-4244-0591-2}, } @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 = {Proceedings of the 1st International Conference on Virtual Execution Environments, VEE 2005, Chicago, IL, USA, June 11-12, 2005}, editor = {Michael Hind and Jan Vitek}, publisher = {ACM}, isbn = {1-59593-047-7}, } @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 Notices}, 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 = {Theoretical Computer Science}, 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 = {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}, } @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 = {Journal of Functional Programming}, 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 = {Types in Compilation, Second International Workshop, TIC 98, Kyoto, Japan, March 25-27, 1998, Proceedings}, editor = {Xavier Leroy and Atsushi Ohori}, volume = {1473}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-64925-5}, } @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 = {Higher-Order and Symbolic Computation}, 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 Computing Surveys}, 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 = {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}, } @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 = {Proceedings of the IEEE Symposium on Visual Analytics Science and Technology, IEEE VAST 2008, Columbus, Ohio, USA, 19-24 October 2008}, publisher = {IEEE}, } @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 = {Theoretical Computer Science}, 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 = {The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013}, editor = {Roberto Giacobazzi and Radhia Cousot}, publisher = {ACM}, isbn = {978-1-4503-1832-7}, } @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 = {Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009}, editor = {Graham Hutton and Andrew P. Tolmach}, publisher = {ACM}, isbn = {978-1-60558-332-7}, } @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 Notices}, 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 = {IEEE Computer Graphics and Applications}, 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 = {Journal of Functional Programming}, 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 = {Proceedings of the 40th SIGCSE Technical Symposium on Computer Science Education, SIGCSE 2009, Chattanooga, TN, USA, March 4-7, 2009}, editor = {Sue Fitzgerald and Mark Guzdial and Gary Lewandowski and Steven A. Wolfman}, publisher = {ACM}, isbn = {978-1-60558-183-5}, } @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 = {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}, } @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 = {Journal of Functional Programming}, 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 = {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}, } @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 = {Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003}, editor = {Colin Runciman and Olin Shivers}, publisher = {ACM}, isbn = {1-58113-756-7}, } @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 = {Electronic Notes in Theoretical Computer Science}, 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 = {Challenges and Opportunities of HealthGrids - Proceedings of Healthgrid 2006, Valencia, Spain, 7-9 June, 2006}, editor = {Vicente Hernández and Ignacio Blanquer and Tony Solomonides and Vincent Breton and Yannick Legré}, volume = {120}, series = {Studies in Health Technology and Informatics}, publisher = {IOS Press}, isbn = {978-1-58603-617-1}, } @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 = {Proceedings of the ACM on Programming Languages}, 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 Computing Surveys}, 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 = {Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming}, series = {ICFP '01}, address = {New York, NY, USA}, publisher = {Association for Computing Machinery}, } @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 = {ACM Transactions on Programming Languages and Systems}, 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 = {Information Visualization}, 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 = {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 = {Hongseok Yang}, volume = {10201}, series = {Lecture Notes in Computer Science}, isbn = {978-3-662-54434-1}, } @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 = {Higher-Order and Symbolic Computation}, 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 Notices}, 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 = {Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings}, editor = {C.-H. Luke Ong}, volume = {3634}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-28231-9}, } @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 = {Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010}, editor = {Andrew Kennedy and Nick Benton}, publisher = {ACM}, isbn = {978-1-60558-891-9}, } @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 = {Proceedings of TLDI 03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003}, editor = {Zhong Shao and Peter Lee}, publisher = {ACM}, isbn = {1-58113-649-8}, } @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 = {Inf. Process. Lett.}, 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 = {Grid Computing - GRID 2002, Third International Workshop, Baltimore, MD, USA, November 18, 2002, Proceedings}, editor = {Manish Parashar}, volume = {2536}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-00133-6}, } @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 = {Journal of Logic and Computation}, 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 = {Journal of the ACM}, 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 = {ACM Transactions on Programming Languages and Systems}, 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 = {Theoretical Aspects of Computer Software, Third International Symposium, TACS 97, Sendai, Japan, September 23-26, 1997, Proceedings}, editor = {Martín Abadi and Takayasu Ito}, volume = {1281}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-63388-X}, } @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 = {Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings}, editor = {David H. Pitt and David E. Rydeheard and Peter Dybjer and Andrew M. Pitts and Axel Poigné}, volume = {389}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-51662-X}, } @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 = {Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005}, editor = {Olivier Danvy and Benjamin C. Pierce}, publisher = {ACM}, isbn = {1-59593-064-7}, } @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 = {Microprocessors and Microsystems}, 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 2009: Proceedings of the 21st Annual ACM Symposium on Parallel Algorithms and Architectures, Calgary, Alberta, Canada, August 11-13, 2009}, editor = {Friedhelm Meyer auf der Heide and Michael A. Bender}, publisher = {ACM}, isbn = {978-1-60558-606-9}, } @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 = {Proceedings of the ACM on Programming Languages}, 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 = {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}, } @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 = {Proceedings of the Joint International Conference on Measurement and Modeling of Computer Systems, SIGMETRICS/Performance 2006, Saint Malo, France, June 26-30, 2006}, editor = {Raymond A. Marie and Peter B. Key and Evgenia Smirni}, publisher = {ACM}, isbn = {1-59593-319-0}, } @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 = {Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009}, editor = {Thorsten Altenkirch and Todd D. Millstein}, publisher = {ACM}, isbn = {978-1-60558-330-3}, } @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 = {Proceedings of the Conference on Designing Interactive Systems, Cape Town, South Africa, February 25-27, 2008}, editor = {Johann van der Schijff and Gary Marsden}, publisher = {ACM}, isbn = {978-1-60558-002-9}, } @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 = {Journal of Functional Programming}, 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 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 = {Josep Díaz and Fernando Orejas}, volume = {352}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-50940-2}, } @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 = {Informatics - 10 Years Back. 10 Years Ahead}, editor = {Reinhard Wilhelm}, volume = {2000}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-41635-8}, } @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 = {Journal of Functional Programming}, 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 = {Proceedings of the ACM on Programming Languages}, 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 News}, 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 Notices}, 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 = {Higher-Order and Symbolic Computation}, 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 = {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 = {Jeremy Avigad and Assia Mahboubi}, volume = {10895}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-319-94821-8}, } @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 = {Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings}, editor = {Pierre-Louis Curien}, volume = {5608}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-02272-2}, } @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 = {Theoretical Computer Science}, 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 = {Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming}, series = {ICFP '01}, address = {New York, NY, USA}, publisher = {Association for Computing Machinery}, } @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 = {Annals of Pure and Applied Logic}, 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 = {Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings}, editor = {Josep Díaz and Juhani Karhumäki and Arto Lepistö and Donald Sannella}, volume = {3142}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-22849-7}, } @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 = {Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers}, editor = {Gilles Barthe and Cédric Fournet}, volume = {4912}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-78662-7}, } @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 = {Inf. Comput.}, 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 = {Data Types and Persistence. Edited Papers from the Proceedings of the First Workshop on Persistent Objects, Appin, Scotland, August 1985}, editor = {Malcolm P. Atkinson and Peter Buneman and Ronald Morrison}, series = {Topics in Information Systems}, publisher = {Springer}, isbn = {3-540-18785-5}, } @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 = {Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012}, editor = {John Field and Michael Hicks}, publisher = {ACM}, isbn = {978-1-4503-1083-3}, } @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 = {Journal of Symbolic Computation}, 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 = {Journal of Functional Programming}, 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 = {Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014}, editor = {Johan Jeuring and Manuel M. T. Chakravarty}, publisher = {ACM}, isbn = {978-1-4503-2873-9}, } @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 = {LISP and Functional Programming}, } @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 = {Journal of Functional Programming}, 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 = {Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011}, editor = {Thomas Ball and Mooly Sagiv}, publisher = {ACM}, isbn = {978-1-4503-0490-0}, } @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 = {Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, } @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 = {Inf. Process. Lett.}, 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 = {Proof, Language, and Interaction, Essays in Honour of Robin Milner}, editor = {Gordon D. Plotkin and Colin Stirling and Mads Tofte}, publisher = {The MIT Press}, isbn = {978-0-262-16188-6}, } @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 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 = {Hartmut Ehrig and Robert A. Kowalski and Giorgio Levi and Ugo Montanari}, volume = {250}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-17611-X}, } @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 = {ACM Transactions on Programming Languages and Systems}, 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 = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, } @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 = {Journal of Functional Programming}, 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 News}, 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 = {ACM Trans. Comput. Log.}, 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}, note = {SIGPLAN Notices 31(6), June 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}, }