publications: - title: "A type system for higher-order modules" author: - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2003" doi: "http://doi.acm.org/10.1145/640128.604151" abstract: "We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class values. Our type system harmonizes design elements from previous work, resulting in a simple, economical account of modular programming. The main unifying principle is the treatment of abstraction mechanisms as computational effects. Our language is the first to provide a complete and practical formalization of all of these critical issues in module system design." links: doi: "http://doi.acm.org/10.1145/640128.604151" tags: - "type system" researchr: "https://researchr.org/publication/DreyerCH03" cites: 0 citedby: 0 pages: "236-249" booktitle: "POPL" kind: "inproceedings" key: "DreyerCH03" - title: "Internal Parametricity for Cubical Type Theory" author: - name: "Evan Cavallo" link: "https://researchr.org/alias/evan-cavallo" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2021" doi: "https://doi.org/10.46298/lmcs-17(4:5)2021" links: doi: "https://doi.org/10.46298/lmcs-17(4:5)2021" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lmcs/CavalloH21" researchr: "https://researchr.org/publication/CavalloH21" cites: 0 citedby: 0 journal: "lmcs" volume: "17" number: "4" kind: "article" key: "CavalloH21" - title: "Logical Relations as Types: Proof-Relevant Parametricity for Program Modules" author: - name: "Jonathan Sterling" link: "https://researchr.org/alias/jonathan-sterling" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2021" doi: "https://doi.org/10.1145/3474834" links: doi: "https://doi.org/10.1145/3474834" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jacm/SterlingH21" researchr: "https://researchr.org/publication/SterlingH21" cites: 0 citedby: 0 journal: "JACM" volume: "68" number: "6" kind: "article" key: "SterlingH21" - title: "Responsive parallel computation: bridging competitive and cooperative threading" author: - name: "Stefan K. Muller" link: "https://researchr.org/alias/stefan-k.-muller" - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2017" doi: "http://doi.acm.org/10.1145/3062341.3062370" links: doi: "http://doi.acm.org/10.1145/3062341.3062370" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/MullerA017" researchr: "https://researchr.org/publication/MullerA017" cites: 0 citedby: 0 pages: "677-692" booktitle: "PLDI" kind: "inproceedings" key: "MullerA017" - title: "Cache efficient functional algorithms" author: - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2015" doi: "http://doi.acm.org/10.1145/2776825" links: doi: "http://doi.acm.org/10.1145/2776825" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/cacm/BlellochH15" researchr: "https://researchr.org/publication/BlellochH15" cites: 0 citedby: 0 journal: "CACM" volume: "58" number: "7" pages: "101-108" kind: "article" key: "BlellochH15" - title: "Typed Closure Conversion for Recursively-Defined Functions" author: - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1997" doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#020" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#020" researchr: "https://researchr.org/publication/MorrisettH97" cites: 0 citedby: 0 journal: "ENTCS" volume: "10" pages: "230-241" kind: "article" key: "MorrisettH97" - title: "A Framework for Defining Logics" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Furio Honsell" link: "https://researchr.org/alias/furio-honsell" - name: "Gordon D. Plotkin" link: "https://researchr.org/alias/gordon-d.-plotkin" year: "1987" tags: - "logic" researchr: "https://researchr.org/publication/HarperHP87" cites: 0 citedby: 0 pages: "194-204" booktitle: "lics" kind: "inproceedings" key: "HarperHP87" - title: "Structure and Representation in LF" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Donald Sannella" link: "http://homepages.inf.ed.ac.uk/dts/" - name: "Andrzej Tarlecki" link: "https://researchr.org/alias/andrzej-tarlecki" year: "1989" researchr: "https://researchr.org/publication/HarperST89%3A0" cites: 0 citedby: 0 pages: "226-237" booktitle: "lics" kind: "inproceedings" key: "HarperST89:0" - title: "The PsyGrid Experience: Using Web Services in the Study of Schizophrenia" author: - name: "John D. Ainsworth" link: "https://researchr.org/alias/john-d.-ainsworth" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2007" doi: "http://www.igi-global.com/Bookstore/Article.aspx?TitleId=2201" links: doi: "http://www.igi-global.com/Bookstore/Article.aspx?TitleId=2201" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/ijhisi/AinsworthH07" tags: - "web service" - "web services" researchr: "https://researchr.org/publication/AinsworthH07" cites: 0 citedby: 0 journal: "ijhisi" volume: "2" number: "2" pages: "1-20" kind: "article" key: "AinsworthH07" - title: "Space profiling for parallel functional programs" author: - name: "Daniel Spoonhower" link: "https://researchr.org/alias/daniel-spoonhower" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Phillip B. Gibbons" link: "https://researchr.org/alias/phillip-b.-gibbons" year: "2008" doi: "http://doi.acm.org/10.1145/1411204.1411240" links: doi: "http://doi.acm.org/10.1145/1411204.1411240" tags: - "functional programming" - "parallel programming" - "e-science" researchr: "https://researchr.org/publication/SpoonhowerBHG08" cites: 0 citedby: 0 pages: "253-264" booktitle: "ICFP" kind: "inproceedings" key: "SpoonhowerBHG08" - title: "Correcting computer-based assessments for guessing" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2003" doi: "http://dx.doi.org/10.1046/j.0266-4909.2002.00001.x" links: doi: "http://dx.doi.org/10.1046/j.0266-4909.2002.00001.x" tags: - "rule-based" researchr: "https://researchr.org/publication/Harper03%3A2" cites: 0 citedby: 0 journal: "jcal" volume: "19" number: "1" pages: "2-8" kind: "article" key: "Harper03:2" - title: "A separation logic for concurrent randomized programs" author: - name: "Joseph Tassarotti" link: "https://researchr.org/alias/joseph-tassarotti" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2019" doi: "https://dl.acm.org/citation.cfm?id=3290377" links: doi: "https://dl.acm.org/citation.cfm?id=3290377" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/TassarottiH19" researchr: "https://researchr.org/publication/TassarottiH19" cites: 0 citedby: 0 journal: "PACMPL" volume: "3" kind: "article" key: "TassarottiH19" - title: "Resilient cloud computing" author: - name: "Valentina Salapura" link: "https://researchr.org/alias/valentina-salapura" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "M. Viswanathan" link: "https://researchr.org/alias/m.-viswanathan" year: "2013" doi: "http://dx.doi.org/10.1147/JRD.2013.2266972" links: doi: "http://dx.doi.org/10.1147/JRD.2013.2266972" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/ibmrd/SalapuraHV13" researchr: "https://researchr.org/publication/SalapuraHV13" cites: 0 citedby: 0 journal: "ibmrd" volume: "57" number: "5" kind: "article" key: "SalapuraHV13" - title: "A Simplified Account of Polymorphic References" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1994" researchr: "https://researchr.org/publication/Harper94" cites: 0 citedby: 0 journal: "ipl" volume: "51" number: "4" pages: "201-206" kind: "article" key: "Harper94" - title: "PET and the IEEE 488 bus (GPIB): Eugene Fisher & Jensen, Osborne/McGraw-Hill (1980) 233 pp £10.00" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1981" doi: "http://dx.doi.org/10.1016/0141-9331(81)90529-9" links: doi: "http://dx.doi.org/10.1016/0141-9331(81)90529-9" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mam/Harper81" researchr: "https://researchr.org/publication/Harper81" cites: 0 citedby: 0 journal: "mam" volume: "5" number: "1" pages: "36-37" kind: "article" key: "Harper81" - title: "Automatic Generation of Staged Geometric Predicates" author: - name: "Aleksandar Nanevski" link: "https://researchr.org/alias/aleksandar-nanevski" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2003" doi: "http://dx.doi.org/10.1023/A:1025876920522" links: doi: "http://dx.doi.org/10.1023/A:1025876920522" tags: - "e-science" researchr: "https://researchr.org/publication/NanevskiBH03" cites: 0 citedby: 0 journal: "lisp" volume: "16" number: "4" pages: "379-400" kind: "article" key: "NanevskiBH03" - title: "Syntactic Logical Relations for Polymorphic and Recursive Types" author: - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2007" doi: "http://dx.doi.org/10.1016/j.entcs.2007.02.010" links: doi: "http://dx.doi.org/10.1016/j.entcs.2007.02.010" researchr: "https://researchr.org/publication/CraryH07" cites: 0 citedby: 0 journal: "ENTCS" volume: "172" pages: "259-299" kind: "article" key: "CraryH07" - title: "Definition of standard ML" author: - name: "Robin Milner" link: "https://researchr.org/alias/robin-milner" - name: "Mads Tofte" link: "https://researchr.org/alias/mads-tofte" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1990" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0069232" researchr: "https://researchr.org/publication/0069232" cites: 0 citedby: 0 publisher: "MIT Press" isbn: "978-0-262-63132-7" kind: "book" key: "0069232" - title: "Dynamizing static algorithms, with applications to dynamic trees and history independence" author: - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Jorge L. Vittes" link: "https://researchr.org/alias/jorge-l.-vittes" - name: "Shan Leung Maverick Woo" link: "https://researchr.org/alias/shan-leung-maverick-woo" year: "2004" doi: "http://doi.acm.org/10.1145/982792.982871" links: doi: "http://doi.acm.org/10.1145/982792.982871" tags: - "history" researchr: "https://researchr.org/publication/AcarBHVW04" cites: 0 citedby: 0 pages: "531-540" booktitle: "soda" kind: "inproceedings" key: "AcarBHVW04" - title: "From tele ::::presence:::: to human ::::absence::::: the pragmatic construction of the human in communications systems research" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2009" doi: "http://doi.acm.org/10.1145/1671011.1671020" links: doi: "http://doi.acm.org/10.1145/1671011.1671020" researchr: "https://researchr.org/publication/Harper09-0" cites: 0 citedby: 0 pages: "73-82" booktitle: "bcshci" kind: "inproceedings" key: "Harper09-0" - title: "The Essence of ML" author: - name: "John C. Mitchell" link: "https://researchr.org/alias/john-c.-mitchell" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1988" tags: - "C++" researchr: "https://researchr.org/publication/MitchellH88" cites: 0 citedby: 0 pages: "28-46" booktitle: "POPL" kind: "inproceedings" key: "MitchellH88" - title: "A Library for Self-Adjusting Computation" author: - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Matthias Blume" link: "https://researchr.org/alias/matthias-blume" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Kanat Tangwongsan" link: "https://researchr.org/alias/kanat-tangwongsan" year: "2006" doi: "http://dx.doi.org/10.1016/j.entcs.2005.11.043" links: doi: "http://dx.doi.org/10.1016/j.entcs.2005.11.043" researchr: "https://researchr.org/publication/AcarBBHT06" cites: 0 citedby: 0 journal: "ENTCS" volume: "148" number: "2" pages: "127-154" kind: "article" key: "AcarBBHT06" - title: "On equivalence and canonical forms in the LF type theory" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://doi.acm.org/10.1145/1042038.1042041" links: doi: "http://doi.acm.org/10.1145/1042038.1042041" tags: - "type theory" researchr: "https://researchr.org/publication/HarperP05" cites: 0 citedby: 0 journal: "tocl" volume: "6" number: "1" pages: "61-101" kind: "article" key: "HarperP05" - title: "Integrated visual analytics workflow with GeoTime and nSpace VAST 2010 mini challenge 1 award: Outstanding Analysis and Accuracy" author: - name: "Pascale Proulx" link: "https://researchr.org/alias/pascale-proulx" - name: "Adeel Khamisa" link: "https://researchr.org/alias/adeel-khamisa" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2010" doi: "http://dx.doi.org/10.1109/VAST.2010.5653053" links: doi: "http://dx.doi.org/10.1109/VAST.2010.5653053" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/ProulxKH10" tags: - "analysis" - "workflow" researchr: "https://researchr.org/publication/ProulxKH10" cites: 0 citedby: 0 pages: "273-274" booktitle: "ieeevast" kind: "inproceedings" key: "ProulxKH10" - title: "Internal Parametricity for Cubical Type Theory" author: - name: "Evan Cavallo" link: "https://researchr.org/alias/evan-cavallo" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2020" doi: "https://doi.org/10.4230/LIPIcs.CSL.2020.13" links: doi: "https://doi.org/10.4230/LIPIcs.CSL.2020.13" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/Cavallo020" researchr: "https://researchr.org/publication/Cavallo020" cites: 0 citedby: 0 booktitle: "csl" kind: "inproceedings" key: "Cavallo020" - title: "FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2009" doi: "http://dx.doi.org/10.1017/S0956796808007119" links: doi: "http://dx.doi.org/10.1017/S0956796808007119" tags: - "debugging" researchr: "https://researchr.org/publication/Harper09" cites: 0 citedby: 0 journal: "JFP" volume: "19" number: "2" pages: "262" kind: "article" key: "Harper09" - title: "What is a Recursive Module?" author: - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Sidd Puri" link: "https://researchr.org/alias/sidd-puri" year: "1999" doi: "http://doi.acm.org/10.1145/301618.301641" abstract: "A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can impede modular programming by forcing mutually-dependent components to be consolidated into a single module. Recently there have been several proposals for module systems that admit cyclic dependencies, but it is not clear how these proposals relate to one another, nor how one might integrate them into an expressive module system such as that of ML.To address this question we provide a type-theoretic analysis of the notion of a recursive module in the context of a \"phase-distinction\" formalism for higher-order module systems. We extend this calculus with a recursive module mechanism and a new form of signature, called a recursively dependent signature, to support the definition of recursive modules. These extensions are justified by an interpretation in terms of more primitive language constructs. This interpretation may also serve as a guide for implementation." links: doi: "http://doi.acm.org/10.1145/301618.301641" researchr: "https://researchr.org/publication/CraryHP99" cites: 0 citedby: 0 pages: "50-63" booktitle: "PLDI" kind: "inproceedings" key: "CraryHP99" - title: "Towards a mechanized metatheory of standard ML" author: - name: "Daniel K. Lee" link: "https://researchr.org/alias/daniel-k.-lee" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2007" doi: "http://doi.acm.org/10.1145/1190216.1190245" abstract: "We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest. " links: doi: "http://doi.acm.org/10.1145/1190216.1190245" tags: - "programming languages" - "semantics" - "program verification" - "exceptions" - "metatheory" - "programming" - "abstraction" researchr: "https://researchr.org/publication/LeeCH07%3A0" cites: 0 citedby: 0 pages: "173-184" booktitle: "POPL" kind: "inproceedings" key: "LeeCH07:0" - title: "Modular type classes" author: - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" - name: "Gabriele Keller" link: "https://researchr.org/alias/gabriele-keller" year: "2007" doi: "http://doi.acm.org/10.1145/1190216.1190229" links: doi: "http://doi.acm.org/10.1145/1190216.1190229" researchr: "https://researchr.org/publication/DreyerHCK07" cites: 0 citedby: 0 pages: "63-70" booktitle: "POPL" kind: "inproceedings" key: "DreyerHCK07" - title: "TIL: a type-directed, optimizing compiler for ML (with retrospective)" author: - name: "David Tarditi" link: "https://researchr.org/alias/david-tarditi" - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Perry Cheng" link: "https://researchr.org/alias/perry-cheng" - name: "Christopher A. Stone" link: "https://researchr.org/alias/christopher-a.-stone" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1996" doi: "http://doi.acm.org/10.1145/989393.989449" links: doi: "http://doi.acm.org/10.1145/989393.989449" tags: - "optimization" - "compiler" researchr: "https://researchr.org/publication/TarditiMCSHL96a" cites: 0 citedby: 0 pages: "554-567" booktitle: "PLDI" kind: "inproceedings" key: "TarditiMCSHL96a" - title: "Strict bidirectional type checking" author: - name: "Adam J. Chlipala" link: "http://adam.chlipala.net/" - name: "Leaf Petersen" link: "https://researchr.org/alias/leaf-petersen" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2005" doi: "http://doi.acm.org/10.1145/1040294.1040301" links: doi: "http://doi.acm.org/10.1145/1040294.1040301" tags: - "type checking" researchr: "https://researchr.org/publication/ChlipalaPH05" cites: 0 citedby: 0 pages: "71-78" booktitle: "tldi" kind: "inproceedings" key: "ChlipalaPH05" - title: "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities" author: - name: "Carlo Angiuli" link: "https://researchr.org/alias/carlo-angiuli" - name: "Kuen-Bang Hou (Favonia)" link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2018" doi: "https://doi.org/10.4230/LIPIcs.CSL.2018.6" links: doi: "https://doi.org/10.4230/LIPIcs.CSL.2018.6" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/AngiuliF018" researchr: "https://researchr.org/publication/AngiuliF018" cites: 0 citedby: 0 booktitle: "csl" kind: "inproceedings" key: "AngiuliF018" - title: "Syntax and models of Cartesian cubical type theory" author: - name: "Carlo Angiuli" link: "https://researchr.org/alias/carlo-angiuli" - name: "Guillaume Brunerie" link: "https://researchr.org/alias/guillaume-brunerie" - name: "Thierry Coquand" link: "https://researchr.org/alias/thierry-coquand" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Kuen-Bang Hou (Favonia)" link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29" - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" year: "2021" doi: "https://doi.org/10.1017/S0960129521000347" links: doi: "https://doi.org/10.1017/S0960129521000347" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/AngiuliBCHHL21" researchr: "https://researchr.org/publication/AngiuliBCHHL21" cites: 0 citedby: 0 journal: "mscs" volume: "31" number: "4" pages: "424-468" kind: "article" key: "AngiuliBCHHL21" - title: "Selective memoization" author: - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2003" doi: "http://doi.acm.org/10.1145/640128.604133" links: doi: "http://doi.acm.org/10.1145/640128.604133" tags: - "e-science" researchr: "https://researchr.org/publication/AcarBH03" cites: 0 citedby: 0 pages: "14-25" booktitle: "POPL" kind: "inproceedings" key: "AcarBH03" - title: "An overview of the Oregon programming languages summer school" author: - name: "Jim Allen" link: "https://researchr.org/alias/jim-allen" - name: "Zena M. Ariola" link: "https://researchr.org/alias/zena-m.-ariola" - name: "Pierre-Louis Curien" link: "https://researchr.org/alias/pierre-louis-curien" - name: "Matthew Fluet" link: "https://researchr.org/alias/matthew-fluet" - name: "Jeff Foster" link: "https://researchr.org/alias/jeff-foster" - name: "Dan Grossman" link: "https://researchr.org/alias/dan-grossman" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Hugo Herbelin" link: "https://researchr.org/alias/hugo-herbelin" - name: "Yannis Smaragdakis" link: "https://researchr.org/alias/yannis-smaragdakis" - name: "David Walker" link: "https://researchr.org/alias/david-walker" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" year: "2009" doi: "http://doi.acm.org/10.1145/1816027.1816029" links: doi: "http://doi.acm.org/10.1145/1816027.1816029" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/sigplan/AllenACFFGHHSWZ09" researchr: "https://researchr.org/publication/AllenACFFGHHSWZ09" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "44" number: "11" pages: "1-3" kind: "article" key: "AllenACFFGHHSWZ09" - title: "Sheaf Semantics of Termination-Insensitive Noninterference" author: - name: "Jonathan Sterling" link: "https://researchr.org/alias/jonathan-sterling" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2022" doi: "https://doi.org/10.4230/LIPIcs.FSCD.2022.5" links: doi: "https://doi.org/10.4230/LIPIcs.FSCD.2022.5" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fscd/Sterling022" researchr: "https://researchr.org/publication/Sterling022" cites: 0 citedby: 0 booktitle: "fscd" kind: "inproceedings" key: "Sterling022" - title: "Development and integration of a Surveillance Monitoring solution to provide earlier detection of the deteriorating patient" author: - name: "N. Donnelly" link: "https://researchr.org/alias/n.-donnelly" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "D. Branagh" link: "https://researchr.org/alias/d.-branagh" - name: "J. Francey" link: "https://researchr.org/alias/j.-francey" - name: "H. Easlea" link: "https://researchr.org/alias/h.-easlea" - name: "V. Faro-Maza" link: "https://researchr.org/alias/v.-faro-maza" - name: "T. Hunniford" link: "https://researchr.org/alias/t.-hunniford" - name: "A. Mooney" link: "https://researchr.org/alias/a.-mooney" - name: "J. McLaughlin" link: "https://researchr.org/alias/j.-mclaughlin" year: "2015" doi: "http://dx.doi.org/10.1109/EMBC.2015.7318581" links: doi: "http://dx.doi.org/10.1109/EMBC.2015.7318581" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/embc/DonnellyHBFEFHM15" researchr: "https://researchr.org/publication/DonnellyHBFEFHM15" cites: 0 citedby: 0 pages: "1198-1202" booktitle: "embc" kind: "inproceedings" key: "DonnellyHBFEFHM15" - title: "PsyGrid: Applying e-Science to Epidemiology" author: - name: "John Ainsworth" link: "https://researchr.org/alias/john-ainsworth" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Ismael Juma" link: "https://researchr.org/alias/ismael-juma" - name: "Iain E. Buchan" link: "https://researchr.org/alias/iain-e.-buchan" year: "2006" doi: "http://doi.ieeecomputersociety.org/10.1109/CBMS.2006.135" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CBMS.2006.135" tags: - "e-science" researchr: "https://researchr.org/publication/AinsworthHJB06" cites: 0 citedby: 0 pages: "727-732" booktitle: "cbms" kind: "inproceedings" key: "AinsworthHJB06" - title: "Self-adjusting beat detection and prediction in music" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "M. Ed Jernigan" link: "https://researchr.org/alias/m.-ed-jernigan" year: "2004" doi: "http://dx.doi.org/10.1109/ICASSP.2004.1326809" links: doi: "http://dx.doi.org/10.1109/ICASSP.2004.1326809" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icassp/HarperJ04" researchr: "https://researchr.org/publication/HarperJ04" cites: 0 citedby: 0 pages: "245-248" booktitle: "icassp" kind: "inproceedings" key: "HarperJ04" - title: "A separate compilation extension to standard ML" author: - name: "David Swasey" link: "https://researchr.org/alias/david-swasey" - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2006" doi: "http://doi.acm.org/10.1145/1159876.1159883" links: doi: "http://doi.acm.org/10.1145/1159876.1159883" researchr: "https://researchr.org/publication/SwaseyVCH06" cites: 0 citedby: 0 pages: "32-42" booktitle: "ml" kind: "inproceedings" key: "SwaseyVCH06" - title: "On the unusual effectiveness of logic in computer science" author: - name: "Joseph Y. Halpern" link: "https://researchr.org/alias/joseph-y.-halpern" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Neil Immerman" link: "https://researchr.org/alias/neil-immerman" - name: "Phokion G. Kolaitis" link: "https://researchr.org/alias/phokion-g.-kolaitis" - name: "Moshe Y. Vardi" link: "https://researchr.org/alias/moshe-y.-vardi" - name: "Victor Vianu" link: "https://researchr.org/alias/victor-vianu" year: "2001" doi: "http://www.math.ucla.edu/~asl/bsl/0702/0702-003.ps" links: doi: "http://www.math.ucla.edu/~asl/bsl/0702/0702-003.ps" tags: - "e-science" - "logic" researchr: "https://researchr.org/publication/HalpernHIKVV01" cites: 0 citedby: 0 journal: "bsl" volume: "7" number: "2" pages: "213-236" kind: "article" key: "HalpernHIKVV01" - title: "Adaptive functional programming" author: - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2002" doi: "http://doi.acm.org/10.1145/503272.503296" links: doi: "http://doi.acm.org/10.1145/503272.503296" tags: - "functional programming" - "e-science" - "programming" researchr: "https://researchr.org/publication/AcarBH02" cites: 0 citedby: 0 pages: "247-259" booktitle: "POPL" kind: "inproceedings" key: "AcarBH02" - title: "Avian Flu Case Study with nSpace and GeoTime" author: - name: "Pascale Proulx" link: "https://researchr.org/alias/pascale-proulx" - name: "Sumeet Tandon" link: "https://researchr.org/alias/sumeet-tandon" - name: "Adam Bodnar" link: "https://researchr.org/alias/adam-bodnar" - name: "David Schroh" link: "https://researchr.org/alias/david-schroh" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "William Wright" link: "https://researchr.org/alias/william-wright" year: "2006" doi: "http://dx.doi.org/10.1109/VAST.2006.261427" links: doi: "http://dx.doi.org/10.1109/VAST.2006.261427" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/ProulxTBSHW06" tags: - "case study" researchr: "https://researchr.org/publication/ProulxTBSHW06" cites: 0 citedby: 0 pages: "27-34" booktitle: "ieeevast" kind: "inproceedings" key: "ProulxTBSHW06" - title: "Practical Foundations for Programming Languages" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2012" links: "pdf": "http://www.cs.cmu.edu/~rwh/plbook/book.pdf" tags: - "programming languages" researchr: "https://researchr.org/publication/Harper2012" cites: 0 citedby: 0 kind: "book" key: "Harper2012" - title: "Using page residency to balance tradeoffs in tracing garbage collection" author: - name: "Daniel Spoonhower" link: "https://researchr.org/alias/daniel-spoonhower" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2005" doi: "http://doi.acm.org/10.1145/1064979.1064989" links: doi: "http://doi.acm.org/10.1145/1064979.1064989" tags: - "e-science" researchr: "https://researchr.org/publication/SpoonhowerBH05" cites: 0 citedby: 0 pages: "57-67" booktitle: "vee" kind: "inproceedings" key: "SpoonhowerBH05" - title: "Position paper: practical foundations for lrogramming languages" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2008" doi: "http://doi.acm.org/10.1145/1480828.1480843" links: doi: "http://doi.acm.org/10.1145/1480828.1480843" researchr: "https://researchr.org/publication/Harper08" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "43" number: "11" pages: "71-73" kind: "article" key: "Harper08" - title: "A Record Calculus Based on Symmetric Concatenation" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1991" tags: - "rule-based" - "C++" researchr: "https://researchr.org/publication/HarperP91%3A0" cites: 0 citedby: 0 pages: "131-142" booktitle: "POPL" kind: "inproceedings" key: "HarperP91:0" - title: "Type Checking with Universes" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Robert Pollack" link: "https://researchr.org/alias/robert-pollack" year: "1991" tags: - "type checking" researchr: "https://researchr.org/publication/HarperP91" cites: 0 citedby: 0 journal: "TCS" volume: "89" number: "1" pages: "107-136" kind: "article" key: "HarperP91" - title: "Typing First-Class Continuations in ML" author: - name: "Bruce F. Duba" link: "https://researchr.org/alias/bruce-f.-duba" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "David B. MacQueen" link: "https://researchr.org/alias/david-b.-macqueen" year: "1991" researchr: "https://researchr.org/publication/DubaHM91" cites: 0 citedby: 0 pages: "163-173" booktitle: "POPL" kind: "inproceedings" key: "DubaHM91" - title: "Focusing on Binding and Computation" author: - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Noam Zeilberger" link: "https://researchr.org/alias/noam-zeilberger" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2008" doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48" links: doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48" researchr: "https://researchr.org/publication/LicataZH08" cites: 0 citedby: 0 pages: "241-252" booktitle: "lics" kind: "inproceedings" key: "LicataZH08" - title: "Correctness of compiling polymorphism to dynamic typing" author: - name: "Kuen-Bang Hou (Favonia)" link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29" - name: "Nick Benton" link: "https://researchr.org/alias/nick-benton" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2017" doi: "http://dx.doi.org/10.1017/S0956796816000265" links: doi: "http://dx.doi.org/10.1017/S0956796816000265" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/HouBH17" researchr: "https://researchr.org/publication/HouBH17" cites: 0 citedby: 0 journal: "JFP" volume: "27" kind: "article" key: "HouBH17" - title: "How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler" author: - name: "Andrew Bernard" link: "https://researchr.org/alias/andrew-bernard" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1473/14730053.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1473/14730053.htm" tags: - "compiler" researchr: "https://researchr.org/publication/BernardHL98" cites: 0 citedby: 0 pages: "53-77" booktitle: "tic" kind: "inproceedings" key: "BernardHL98" - title: "Polymorphic Type Assignment and CPS Conversion" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Mark Lillibridge" link: "https://researchr.org/alias/mark-lillibridge" year: "1993" researchr: "https://researchr.org/publication/HarperL93%3A0" cites: 0 citedby: 0 journal: "lisp" volume: "6" number: "3-4" pages: "361-380" kind: "article" key: "HarperL93:0" - title: "ML and Beyond" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "John C. Mitchell" link: "https://researchr.org/alias/john-c.-mitchell" year: "1996" tags: - "C++" researchr: "https://researchr.org/publication/HarperM96" cites: 0 citedby: 0 journal: "ACM Comput. Surv." volume: "28" number: "4es" pages: "219" kind: "article" key: "HarperM96" - title: "Abstract Models of Memory Management" author: - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Matthias Felleisen" link: "http://www.ccs.neu.edu/home/matthias/" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1995" tags: - "meta-model" - "memory management" - "Meta-Environment" researchr: "https://researchr.org/publication/MorrisettFH95" cites: 0 citedby: 0 pages: "66-77" booktitle: "fpca" kind: "inproceedings" key: "MorrisettFH95" - title: "Stories in GeoTime" author: - name: "Ryan Eccles" link: "https://researchr.org/alias/ryan-eccles" - name: "Thomas Kapler" link: "https://researchr.org/alias/thomas-kapler" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "William Wright" link: "https://researchr.org/alias/william-wright" year: "2007" doi: "http://dx.doi.org/10.1109/VAST.2007.4388992" links: doi: "http://dx.doi.org/10.1109/VAST.2007.4388992" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/EcclesKHW07" researchr: "https://researchr.org/publication/EcclesKHW07" cites: 0 citedby: 0 pages: "19-26" booktitle: "ieeevast" kind: "inproceedings" key: "EcclesKHW07" - title: "Configurable Spaces: Temporal analysis in diagrammatic contexts" author: - name: "Thomas Kapler" link: "https://researchr.org/alias/thomas-kapler" - name: "Ryan Eccles" link: "https://researchr.org/alias/ryan-eccles" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "William Wright" link: "https://researchr.org/alias/william-wright" year: "2008" doi: "http://dx.doi.org/10.1109/VAST.2008.4677355" links: doi: "http://dx.doi.org/10.1109/VAST.2008.4677355" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ieeevast/KaplerEHW08" tags: - "analysis" - "context-aware" researchr: "https://researchr.org/publication/KaplerEHW08" cites: 0 citedby: 0 pages: "43-50" booktitle: "ieeevast" kind: "inproceedings" key: "KaplerEHW08" - title: "Exception tracking in an open world" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2018" doi: "https://doi.org/10.1016/j.tcs.2018.02.032" links: doi: "https://doi.org/10.1016/j.tcs.2018.02.032" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tcs/Harper18" researchr: "https://researchr.org/publication/Harper18" cites: 0 citedby: 0 journal: "TCS" volume: "741" pages: "25-31" kind: "article" key: "Harper18" - title: "Cache and I/O efficent functional algorithms" author: - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2013" doi: "http://doi.acm.org/10.1145/2429069.2429077" links: doi: "http://doi.acm.org/10.1145/2429069.2429077" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/BlellochH13" researchr: "https://researchr.org/publication/BlellochH13" cites: 0 citedby: 0 pages: "39-50" booktitle: "POPL" kind: "inproceedings" key: "BlellochH13" - title: "A universe of binding and computation" author: - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2009" doi: "http://doi.acm.org/10.1145/1596550.1596571" links: doi: "http://doi.acm.org/10.1145/1596550.1596571" researchr: "https://researchr.org/publication/LicataH09" cites: 0 citedby: 0 pages: "123-134" booktitle: "ICFP" kind: "inproceedings" key: "LicataH09" - title: "An effective theory of type refinements" author: - name: "Yitzhak Mandelbaum" link: "https://researchr.org/alias/yitzhak-mandelbaum" - name: "David Walker" link: "https://researchr.org/alias/david-walker" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2003" doi: "http://doi.acm.org/10.1145/944746.944725" links: doi: "http://doi.acm.org/10.1145/944746.944725" tags: - "refinement" - "type theory" researchr: "https://researchr.org/publication/MandelbaumWH03-0" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "38" number: "9" pages: "213-225" kind: "article" key: "MandelbaumWH03-0" - title: "nSpace and GeoTime: A VAST 2006 Case Study" author: - name: "Pascale Proulx" link: "https://researchr.org/alias/pascale-proulx" - name: "Lynn Chien" link: "https://researchr.org/alias/lynn-chien" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "David Schroh" link: "https://researchr.org/alias/david-schroh" - name: "Thomas Kapler" link: "https://researchr.org/alias/thomas-kapler" - name: "David Jonker" link: "https://researchr.org/alias/david-jonker" - name: "William Wright" link: "https://researchr.org/alias/william-wright" year: "2007" doi: "http://doi.ieeecomputersociety.org/10.1109/MCG.2007.131" links: doi: "http://doi.ieeecomputersociety.org/10.1109/MCG.2007.131" tags: - "case study" researchr: "https://researchr.org/publication/ProulxCHSKJW07" cites: 0 citedby: 0 journal: "cga" volume: "27" number: "5" pages: "46-56" kind: "article" key: "ProulxCHSKJW07" - title: "Proof-Directed Debugging" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1999" tags: - "debugging" researchr: "https://researchr.org/publication/Harper99%3A0" cites: 0 citedby: 0 journal: "JFP" volume: "9" number: "4" pages: "463-469" kind: "article" key: "Harper99:0" - title: "Higher-Order Modules and the Phase Distinction" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "John C. Mitchell" link: "https://researchr.org/alias/john-c.-mitchell" - name: "Eugenio Moggi" link: "https://researchr.org/alias/eugenio-moggi" year: "1990" tags: - "C++" researchr: "https://researchr.org/publication/HarperMM90" cites: 0 citedby: 0 pages: "341-354" booktitle: "POPL" kind: "inproceedings" key: "HarperMM90" - title: "Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report" author: - name: "Mark W. Bailey" link: "https://researchr.org/alias/mark-w.-bailey" - name: "Kim B. Bruce" link: "https://researchr.org/alias/kim-b.-bruce" - name: "Kathleen Fisher" link: "http://www.research.att.com/people/Fisher_Kathleen_S" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Stuart Reges" link: "https://researchr.org/alias/stuart-reges" year: "2009" doi: "http://doi.acm.org/10.1145/1508865.1508913" links: doi: "http://doi.acm.org/10.1145/1508865.1508913" tags: - "programming languages" - "programming" researchr: "https://researchr.org/publication/BaileyBFHR09" cites: 0 citedby: 0 pages: "132-133" booktitle: "sigcse" kind: "inproceedings" key: "BaileyBFHR09" - title: "A Symmetric Modal Lambda Calculus for Distributed Computing" author: - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2004" doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm" links: doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm" researchr: "https://researchr.org/publication/VIICHP04" cites: 0 citedby: 0 pages: "286-295" booktitle: "lics" kind: "inproceedings" key: "VIICHP04" - title: "Typing First-Class Continuations in ML" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Bruce F. Duba" link: "https://researchr.org/alias/bruce-f.-duba" - name: "David B. MacQueen" link: "https://researchr.org/alias/david-b.-macqueen" year: "1993" researchr: "https://researchr.org/publication/HarperDM93" cites: 0 citedby: 0 journal: "JFP" volume: "3" number: "4" pages: "465-484" kind: "article" key: "HarperDM93" - title: "Silent Data Corruption - Myth or reality?" author: - name: "Cristian Constantinescu" link: "https://researchr.org/alias/cristian-constantinescu" - name: "Ishwar Parulkar" link: "https://researchr.org/alias/ishwar-parulkar" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Sarah Michalak" link: "https://researchr.org/alias/sarah-michalak" year: "2008" doi: "http://dx.doi.org/10.1109/DSN.2008.4630077" links: doi: "http://dx.doi.org/10.1109/DSN.2008.4630077" tags: - "data-flow" researchr: "https://researchr.org/publication/ConstantinescuPHM08" cites: 0 citedby: 0 pages: "108-109" booktitle: "dsn" kind: "inproceedings" key: "ConstantinescuPHM08" - title: "An effective theory of type refinements" author: - name: "Yitzhak Mandelbaum" link: "https://researchr.org/alias/yitzhak-mandelbaum" - name: "David Walker" link: "https://researchr.org/alias/david-walker" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2003" doi: "http://doi.acm.org/10.1145/944705.944725" links: doi: "http://doi.acm.org/10.1145/944705.944725" tags: - "refinement" - "type theory" researchr: "https://researchr.org/publication/MandelbaumWH03" cites: 0 citedby: 0 pages: "213-225" booktitle: "ICFP" kind: "inproceedings" key: "MandelbaumWH03" - title: "2-Dimensional Directed Type Theory" author: - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2011" doi: "http://dx.doi.org/10.1016/j.entcs.2011.09.026" links: doi: "http://dx.doi.org/10.1016/j.entcs.2011.09.026" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/LicataH11" researchr: "https://researchr.org/publication/LicataH11" cites: 0 citedby: 0 journal: "ENTCS" volume: "276" pages: "263-289" kind: "article" key: "LicataH11" - title: "Design and implementation of security in a data collection system for epidemiology" author: - name: "John D. Ainsworth" link: "https://researchr.org/alias/john-d.-ainsworth" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Ismael Juma" link: "https://researchr.org/alias/ismael-juma" - name: "Iain E. Buchan" link: "https://researchr.org/alias/iain-e.-buchan" year: "2006" doi: "http://www.booksonline.iospress.nl/Content/View.aspx?piid=4754" links: doi: "http://www.booksonline.iospress.nl/Content/View.aspx?piid=4754" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/healthgrid/AinsworthHJB06" researchr: "https://researchr.org/publication/AinsworthHJB06-0" cites: 0 citedby: 0 pages: "348-357" booktitle: "healthgrid" kind: "inproceedings" key: "AinsworthHJB06-0" - title: "Competitive parallelism: getting your priorities right" author: - name: "Stefan K. Muller" link: "https://researchr.org/alias/stefan-k.-muller" - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2018" doi: "https://doi.org/10.1145/3236790" links: doi: "https://doi.org/10.1145/3236790" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/MullerA018" researchr: "https://researchr.org/publication/MullerA018" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "ICFP" kind: "article" key: "MullerA018" - title: "A type theory for memory allocation and data layout" author: - name: "Leaf Petersen" link: "https://researchr.org/alias/leaf-petersen" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://doi.acm.org/10.1145/640128.604147" links: doi: "http://doi.acm.org/10.1145/640128.604147" tags: - "layout" - "data-flow" - "type theory" researchr: "https://researchr.org/publication/PetersenHCP03" cites: 0 citedby: 0 pages: "172-184" booktitle: "POPL" kind: "inproceedings" key: "PetersenHCP03" - title: "Research in Programming Languages for Composability, Safety, and Performance" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1996" tags: - "programming languages" - "programming" researchr: "https://researchr.org/publication/HarperL96" cites: 0 citedby: 0 journal: "ACM Comput. Surv." volume: "28" number: "4es" pages: "195" kind: "article" key: "HarperL96" - title: "Automatic Generation of Staged Geometric Predicates" author: - name: "Aleksandar Nanevski" link: "https://researchr.org/alias/aleksandar-nanevski" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2001" tags: - "e-science" researchr: "https://researchr.org/publication/NanevskiBH01" cites: 0 citedby: 0 pages: "217-228" booktitle: "ICFP" kind: "inproceedings" key: "NanevskiBH01" - title: "Adaptive functional programming" author: - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2006" doi: "http://doi.acm.org/10.1145/1186634" links: doi: "http://doi.acm.org/10.1145/1186634" tags: - "functional programming" - "e-science" - "programming" researchr: "https://researchr.org/publication/AcarBH06" cites: 0 citedby: 0 journal: "TOPLAS" volume: "28" number: "6" pages: "990-1034" kind: "article" key: "AcarBH06" - title: "Stories in GeoTime" author: - name: "Ryan Eccles" link: "https://researchr.org/alias/ryan-eccles" - name: "Thomas Kapler" link: "https://researchr.org/alias/thomas-kapler" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "William Wright" link: "https://researchr.org/alias/william-wright" year: "2008" doi: "http://dx.doi.org/10.1057/palgrave.ivs.9500173" links: doi: "http://dx.doi.org/10.1057/palgrave.ivs.9500173" researchr: "https://researchr.org/publication/EcclesKHW08" cites: 0 citedby: 0 journal: "ivs" volume: "7" number: "1" pages: "3-17" kind: "article" key: "EcclesKHW08" - title: "A Higher-Order Logic for Concurrent Termination-Preserving Refinement" author: - name: "Joseph Tassarotti" link: "https://researchr.org/alias/joseph-tassarotti" - name: "Ralf Jung" link: "https://researchr.org/alias/ralf-jung" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2017" doi: "http://dx.doi.org/10.1007/978-3-662-54434-1_34" links: doi: "http://dx.doi.org/10.1007/978-3-662-54434-1_34" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/TassarottiJ017" researchr: "https://researchr.org/publication/TassarottiJ017" cites: 0 citedby: 0 pages: "909-936" booktitle: "ESOP" kind: "inproceedings" key: "TassarottiJ017" - title: "A Network Protocol Stack in Standard ML" author: - name: "Edoardo Biagioni" link: "https://researchr.org/alias/edoardo-biagioni" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "2001" tags: - "protocol" researchr: "https://researchr.org/publication/BiagioniHL01" cites: 0 citedby: 0 journal: "lisp" volume: "14" number: "4" pages: "309-356" kind: "article" key: "BiagioniHL01" - title: "ML and Beyond" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "John C. Mitchell" link: "https://researchr.org/alias/john-c.-mitchell" year: "1997" tags: - "C++" researchr: "https://researchr.org/publication/HarperM97" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "32" number: "1" pages: "80-85" kind: "article" key: "HarperM97" - title: "Distributed Control Flow with Classical Modal Logic" author: - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2005" doi: "http://dx.doi.org/10.1007/11538363_6" links: doi: "http://dx.doi.org/10.1007/11538363_6" tags: - "modal logic" - "data-flow" - "logic" researchr: "https://researchr.org/publication/VIICH05" cites: 0 citedby: 0 pages: "51-69" booktitle: "csl" kind: "inproceedings" key: "VIICH05" - title: "Distributed programming with distributed authorization" author: - name: "Kumar Avijit" link: "https://researchr.org/alias/kumar-avijit" - name: "Anupam Datta" link: "https://researchr.org/alias/anupam-datta" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2010" doi: "http://doi.acm.org/10.1145/1708016.1708021" links: doi: "http://doi.acm.org/10.1145/1708016.1708021" tags: - "programming" researchr: "https://researchr.org/publication/AvijitDH10" cites: 0 citedby: 0 pages: "27-38" booktitle: "tldi" kind: "inproceedings" key: "AvijitDH10" - title: "Typed compilation of recursive datatypes" author: - name: "Joseph Vanderwaart" link: "https://researchr.org/alias/joseph-vanderwaart" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" - name: "Leaf Petersen" link: "https://researchr.org/alias/leaf-petersen" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Perry Cheng" link: "https://researchr.org/alias/perry-cheng" year: "2003" doi: "http://doi.acm.org/10.1145/604174.604187" links: doi: "http://doi.acm.org/10.1145/604174.604187" researchr: "https://researchr.org/publication/VanderwaartDPCHC03" cites: 0 citedby: 0 pages: "98-108" booktitle: "tldi" kind: "inproceedings" key: "VanderwaartDPCHC03" - title: "Aspects of the Implementation of Type Theory" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1985" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/us/Harper85" researchr: "https://researchr.org/publication/us-153" cites: 0 citedby: 0 school: "Cornell University, USA" kind: "phdthesis" key: "us-153" - title: "A Note on A Simplified Account of Polymorphic References " author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1996" doi: "http://dx.doi.org/10.1016/0020-0190(95)00178-6" links: doi: "http://dx.doi.org/10.1016/0020-0190(95)00178-6" researchr: "https://researchr.org/publication/Harper96" cites: 0 citedby: 0 journal: "ipl" volume: "57" number: "1" pages: "15-16" kind: "article" key: "Harper96" - title: "Trustless Grid Computing in ConCert" author: - name: "Bor-Yuh Evan Chang" link: "https://researchr.org/alias/bor-yuh-evan-chang" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Margaret DeLap" link: "https://researchr.org/alias/margaret-delap" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Jason Liszka" link: "https://researchr.org/alias/jason-liszka" - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm" researchr: "https://researchr.org/publication/ChangCDHLVP02" cites: 0 citedby: 0 pages: "112-125" booktitle: "ccgrid" kind: "inproceedings" key: "ChangCDHLVP02" - title: "A Module System for a Programming Language Based on the LF Logical Framework" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" tags: - "programming languages" - "rule-based" - "programming" researchr: "https://researchr.org/publication/HarperP98" cites: 0 citedby: 0 journal: "logcom" volume: "8" number: "1" pages: "5-31" kind: "article" key: "HarperP98" - title: "A Framework for Defining Logics" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Furio Honsell" link: "https://researchr.org/alias/furio-honsell" - name: "Gordon D. Plotkin" link: "http://homepages.inf.ed.ac.uk/gdp/" year: "1993" doi: "http://doi.acm.org/10.1145/138027.138060" links: doi: "http://doi.acm.org/10.1145/138027.138060" tags: - "logic" researchr: "https://researchr.org/publication/HarperHP93" cites: 0 citedby: 0 journal: "JACM" volume: "40" number: "1" pages: "143-184" kind: "article" key: "HarperHP93" - title: "On the Type Structure of Standard ML" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "John C. Mitchell" link: "https://researchr.org/alias/john-c.-mitchell" year: "1993" doi: "http://doi.acm.org/10.1145/169701.169696" links: doi: "http://doi.acm.org/10.1145/169701.169696" tags: - "C++" researchr: "https://researchr.org/publication/HarperM93" cites: 0 citedby: 0 journal: "TOPLAS" volume: "15" number: "2" pages: "211-252" kind: "article" key: "HarperM93" - title: "TIL: A Type-Directed Optimizing Compiler for ML" author: - name: "David Tarditi" link: "https://researchr.org/alias/david-tarditi" - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Perry Cheng" link: "https://researchr.org/alias/perry-cheng" - name: "Christopher A. Stone" link: "https://researchr.org/alias/christopher-a.-stone" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1996" tags: - "optimization" - "compiler" researchr: "https://researchr.org/publication/TarditiMCSHL96" cites: 0 citedby: 0 pages: "181-192" booktitle: "PLDI" kind: "inproceedings" key: "TarditiMCSHL96" - title: "Relational Interpretations of Recursive Types in an operational Setting (Summary)" author: - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1997" researchr: "https://researchr.org/publication/BirkedalH97" cites: 0 citedby: 0 pages: "458-490" booktitle: "tacs" kind: "inproceedings" key: "BirkedalH97" - title: "Logic Representation in LF" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Donald Sannella" link: "http://homepages.inf.ed.ac.uk/dts/" - name: "Andrzej Tarlecki" link: "https://researchr.org/alias/andrzej-tarlecki" year: "1989" tags: - "logic" researchr: "https://researchr.org/publication/HarperST89" cites: 0 citedby: 0 pages: "250-272" booktitle: "ctcs" kind: "inproceedings" key: "HarperST89" - title: "Typed Closure Conversion" author: - name: "Yasuhiko Minamide" link: "https://researchr.org/alias/yasuhiko-minamide" - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1996" doi: "http://doi.acm.org/10.1145/237721.237791" links: doi: "http://doi.acm.org/10.1145/237721.237791" researchr: "https://researchr.org/publication/MinamideMH96" cites: 0 citedby: 0 pages: "271-283" booktitle: "POPL" kind: "inproceedings" key: "MinamideMH96" - title: "Mechanizing the meta-theory of programming languages" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2005" doi: "http://doi.acm.org/10.1145/1086365.1086396" links: doi: "http://doi.acm.org/10.1145/1086365.1086396" tags: - "programming languages" - "meta programming" - "meta-model" - "programming" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/Harper05%3A0" cites: 0 citedby: 0 pages: "240" booktitle: "ICFP" kind: "inproceedings" key: "Harper05:0" - title: "Microprocessor-based multichannel analyser developed using POLYFORTH" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1983" doi: "http://dx.doi.org/10.1016/0141-9331(83)90328-9" links: doi: "http://dx.doi.org/10.1016/0141-9331(83)90328-9" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mam/Harper83" researchr: "https://researchr.org/publication/Harper83" cites: 0 citedby: 0 journal: "mam" volume: "7" number: "5" pages: "217-222" kind: "article" key: "Harper83" - title: "Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures" author: - name: "Daniel Spoonhower" link: "https://researchr.org/alias/daniel-spoonhower" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Phillip B. Gibbons" link: "https://researchr.org/alias/phillip-b.-gibbons" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2009" doi: "http://doi.acm.org/10.1145/1583991.1584019" links: doi: "http://doi.acm.org/10.1145/1583991.1584019" tags: - "e-science" researchr: "https://researchr.org/publication/SpoonhowerBGH09" cites: 0 citedby: 0 pages: "91-100" booktitle: "spaa" kind: "inproceedings" key: "SpoonhowerBGH09" - title: "Higher inductive types in cubical computational type theory" author: - name: "Evan Cavallo" link: "https://researchr.org/alias/evan-cavallo" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2019" doi: "https://dl.acm.org/citation.cfm?id=3290314" links: doi: "https://dl.acm.org/citation.cfm?id=3290314" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CavalloH19" researchr: "https://researchr.org/publication/CavalloH19" cites: 0 citedby: 0 journal: "PACMPL" volume: "3" kind: "article" key: "CavalloH19" - title: "Self-Adjusting Computation" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2004" doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920254abs.htm" links: doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920254abs.htm" researchr: "https://researchr.org/publication/Harper04%3A0" cites: 0 citedby: 0 pages: "254-255" booktitle: "lics" kind: "inproceedings" key: "Harper04:0" - title: "Consolidating clients on back-end servers with co-location and frequency control" author: - name: "Yiyu Chen" link: "https://researchr.org/alias/yiyu-chen" - name: "Amitayu Das" link: "https://researchr.org/alias/amitayu-das" - name: "Anand Sivasubramaniam" link: "https://researchr.org/alias/anand-sivasubramaniam" - name: "Qian Wang" link: "https://researchr.org/alias/qian-wang" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "M. Bland" link: "https://researchr.org/alias/m.-bland" year: "2006" doi: "http://doi.acm.org/10.1145/1140277.1140331" links: doi: "http://doi.acm.org/10.1145/1140277.1140331" researchr: "https://researchr.org/publication/ChenDSWHB06" cites: 0 citedby: 0 pages: "383-384" booktitle: "sigmetrics" kind: "inproceedings" key: "ChenDSWHB06" - title: "Positively dependent types" author: - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2009" doi: "http://doi.acm.org/10.1145/1481848.1481851" links: doi: "http://doi.acm.org/10.1145/1481848.1481851" researchr: "https://researchr.org/publication/LicataH09-0" cites: 0 citedby: 0 pages: "3-14" booktitle: "plpv" kind: "inproceedings" key: "LicataH09-0" - title: "The past is a different place: they do things differently there" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "D. Randall" link: "https://researchr.org/alias/d.-randall" - name: "N. Smyth" link: "https://researchr.org/alias/n.-smyth" - name: "C. Evans" link: "https://researchr.org/alias/c.-evans" - name: "L. Heledd" link: "https://researchr.org/alias/l.-heledd" - name: "R. Moore" link: "https://researchr.org/alias/r.-moore" year: "2008" doi: "http://doi.acm.org/10.1145/1394445.1394474" links: doi: "http://doi.acm.org/10.1145/1394445.1394474" tags: - "C++" researchr: "https://researchr.org/publication/HarperRSEHM08" cites: 0 citedby: 0 pages: "271-280" booktitle: "ACMdis" kind: "inproceedings" key: "HarperRSEHM08" - title: "Space profiling for parallel functional programs" author: - name: "Daniel Spoonhower" link: "https://researchr.org/alias/daniel-spoonhower" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Phillip B. Gibbons" link: "https://researchr.org/alias/phillip-b.-gibbons" year: "2008" doi: "http://dx.doi.org/10.1017/S0956796810000146" links: doi: "http://dx.doi.org/10.1017/S0956796810000146" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/SpoonhowerBHG08" tags: - "functional programming" - "parallel programming" - "e-science" researchr: "https://researchr.org/publication/SpoonhowerBHG08-0" cites: 0 citedby: 0 journal: "JFP" volume: "20" number: "5-6" pages: "417-461" kind: "article" key: "SpoonhowerBHG08-0" - title: "Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft)" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Robert Pollack" link: "https://researchr.org/alias/robert-pollack" year: "1989" tags: - "type checking" researchr: "https://researchr.org/publication/HarperP89" cites: 0 citedby: 0 pages: "241-256" booktitle: "tapsoft" kind: "inproceedings" key: "HarperP89" - title: "Advanced module systems: a guide for the perplexed (abstract of invited talk)" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://doi.acm.org/10.1145/351240.351252" links: doi: "http://doi.acm.org/10.1145/351240.351252" tags: - "C++" researchr: "https://researchr.org/publication/HarperP00" cites: 0 citedby: 0 pages: "130" booktitle: "ICFP" kind: "inproceedings" key: "HarperP00" - title: "A Language-Based Approach to Security" author: - name: "Fred B. Schneider" link: "https://researchr.org/alias/fred-b.-schneider" - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2000/20000086.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2000/20000086.htm" tags: - "rule-based" - "security" - "systematic-approach" researchr: "https://researchr.org/publication/SchneiderMH01" cites: 0 citedby: 0 pages: "86-101" booktitle: "Dagstuhl" kind: "inproceedings" key: "SchneiderMH01" - title: "Homotopical patch theory" author: - name: "Carlo Angiuli" link: "https://researchr.org/alias/carlo-angiuli" - name: "Edward Morehouse" link: "https://researchr.org/alias/edward-morehouse" - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2016" doi: "http://dx.doi.org/10.1017/S0956796816000198" links: doi: "http://dx.doi.org/10.1017/S0956796816000198" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AngiuliMLH16" researchr: "https://researchr.org/publication/AngiuliMLH16" cites: 0 citedby: 0 journal: "JFP" volume: "26" kind: "article" key: "AngiuliMLH16" - title: "A cost-aware logical framework" author: - name: "Yue Niu" link: "https://researchr.org/alias/yue-niu" - name: "Jonathan Sterling" link: "https://researchr.org/alias/jonathan-sterling" - name: "Harrison Grodin" link: "https://researchr.org/alias/harrison-grodin" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2022" doi: "https://doi.org/10.1145/3498670" links: doi: "https://doi.org/10.1145/3498670" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/NiuSGH22" researchr: "https://researchr.org/publication/NiuSGH22" cites: 0 citedby: 0 journal: "PACMPL" volume: "6" number: "POPL" pages: "1-31" kind: "article" key: "NiuSGH22" - title: "Homotopy type theory: unified foundations of mathematics and computation" author: - name: "Steve Awodey" link: "https://researchr.org/alias/steve-awodey" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2015" doi: "http://doi.acm.org/10.1145/2728816.2728825" links: doi: "http://doi.acm.org/10.1145/2728816.2728825" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/siglog/AwodeyH15" researchr: "https://researchr.org/publication/AwodeyH15" cites: 0 citedby: 0 journal: "siglog" volume: "2" number: "1" pages: "37-44" kind: "article" key: "AwodeyH15" - title: "Compiling Polymorphism Using Intensional Type Analysis" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" year: "1995" tags: - "analysis" - "compiler" researchr: "https://researchr.org/publication/HarperM95" cites: 0 citedby: 0 pages: "130-141" booktitle: "POPL" kind: "inproceedings" key: "HarperM95" - title: "SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations" author: - name: "Eric Allen" link: "https://researchr.org/alias/eric-allen" - name: "Mark W. Bailey" link: "https://researchr.org/alias/mark-w.-bailey" - name: "Rastislav Bodík" link: "https://researchr.org/alias/rastislav-bod%C3%ADk" - name: "Kim B. Bruce" link: "https://researchr.org/alias/kim-b.-bruce" - name: "Kathleen Fisher" link: "http://www.research.att.com/people/Fisher_Kathleen_S" - name: "Stephen N. Freund" link: "https://researchr.org/alias/stephen-n.-freund" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Chandra Krintz" link: "https://researchr.org/alias/chandra-krintz" - name: "Shriram Krishnamurthi" link: "http://www.cs.brown.edu/~sk/" - name: "James R. Larus" link: "https://researchr.org/alias/james-r.-larus" - name: "Doug Lea" link: "https://researchr.org/alias/doug-lea" - name: "Gary T. Leavens" link: "https://researchr.org/alias/gary-t.-leavens" - name: "Lori L. Pollock" link: "https://researchr.org/alias/lori-l.-pollock" - name: "Stuart Reges" link: "https://researchr.org/alias/stuart-reges" - name: "Martin C. Rinard" link: "https://researchr.org/alias/martin-c.-rinard" - name: "Mark Sheldon" link: "https://researchr.org/alias/mark-sheldon" - name: "Franklyn A. Turbak" link: "https://researchr.org/alias/franklyn-a.-turbak" - name: "Mitchell Wand" link: "https://researchr.org/alias/mitchell-wand" year: "2008" doi: "http://doi.acm.org/10.1145/1480828.1480831" links: doi: "http://doi.acm.org/10.1145/1480828.1480831" tags: - "programming languages" - "C++" - "programming" researchr: "https://researchr.org/publication/AllenBBBFFHKKLLLPRRSTW08" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "43" number: "11" pages: "6-29" kind: "article" key: "AllenBBBFFHKKLLLPRRSTW08" - title: "Editorial" author: - name: "David A. Basin" link: "https://researchr.org/alias/david-a.-basin" - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2004" doi: "http://dx.doi.org/10.1023/B:LISP.0000029480.20108.7d" links: doi: "http://dx.doi.org/10.1023/B:LISP.0000029480.20108.7d" researchr: "https://researchr.org/publication/BasinDH04" cites: 0 citedby: 0 journal: "lisp" volume: "17" number: "3" pages: "171" kind: "article" key: "BasinDH04" - title: "Verified Tail Bounds for Randomized Programs" author: - name: "Joseph Tassarotti" link: "https://researchr.org/alias/joseph-tassarotti" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2018" doi: "https://doi.org/10.1007/978-3-319-94821-8_33" links: doi: "https://doi.org/10.1007/978-3-319-94821-8_33" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Tassarotti018" researchr: "https://researchr.org/publication/Tassarotti018" cites: 0 citedby: 0 pages: "560-578" booktitle: "itp" kind: "inproceedings" key: "Tassarotti018" - title: "The Definition of Standard ML, Revised" author: - name: "Milner, Robin" link: "https://researchr.org/alias/milner%2C-robin" - name: "Tofte, Mads" link: "https://researchr.org/alias/tofte%2C-mads" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "MacQueen, David" link: "https://researchr.org/alias/macqueen%2C-david" year: "1997" researchr: "https://researchr.org/publication/Milner1997thedefinition" cites: 0 citedby: 0 address: "Cambridge, MA, USA" publisher: "MIT Press" kind: "book" key: "Milner1997thedefinition" - title: "A Pronominal Approach to Binding and Computation" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Noam Zeilberger" link: "https://researchr.org/alias/noam-zeilberger" year: "2009" doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_2" links: doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_2" tags: - "systematic-approach" researchr: "https://researchr.org/publication/HarperLZ09" cites: 0 citedby: 0 pages: "3-4" booktitle: "tlca" kind: "inproceedings" key: "HarperLZ09" - title: "Automated techniques for provably safe mobile code" author: - name: "Christopher Colby" link: "https://researchr.org/alias/christopher-colby" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" tags: - "mobile code" - "mobile" researchr: "https://researchr.org/publication/ColbyCHLP03" cites: 0 citedby: 0 journal: "TCS" volume: "290" number: "2" pages: "1175-1199" kind: "article" key: "ColbyCHLP03" - title: "A Dependently Typed Assembly Language" author: - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2001" researchr: "https://researchr.org/publication/XiH01" cites: 0 citedby: 0 pages: "169-180" booktitle: "ICFP" kind: "inproceedings" key: "XiH01" - title: "Structured Theory Presentations and Logic Representations" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Donald Sannella" link: "http://homepages.inf.ed.ac.uk/dts/" - name: "Andrzej Tarlecki" link: "https://researchr.org/alias/andrzej-tarlecki" year: "1994" tags: - "logic" researchr: "https://researchr.org/publication/HarperST94" cites: 0 citedby: 0 journal: "APAL" volume: "67" number: "1-3" pages: "113-160" kind: "article" key: "HarperST94" - title: "Self-Adjusting Computation" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2004" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3142&spage=1" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3142&spage=1" researchr: "https://researchr.org/publication/Harper04" cites: 0 citedby: 0 pages: "1-2" booktitle: "icalp" kind: "inproceedings" key: "Harper04" - title: "Type-Safe Distributed Programming with ML5" author: - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_9" links: doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_9" tags: - "programming" researchr: "https://researchr.org/publication/VIICH07" cites: 0 citedby: 0 pages: "108-123" booktitle: "tgc" kind: "inproceedings" key: "VIICH07" - title: "Relational Interpretations of Recursive Types in an Operational Setting" author: - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1999" researchr: "https://researchr.org/publication/BirkedalH99" cites: 0 citedby: 0 journal: "iandc" volume: "155" number: "1-2" pages: "3-63" kind: "article" key: "BirkedalH99" - title: "Modules and Persistence in Standard ML" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1985" doi: "db/conf/db-workshops/Harper85.html" researchr: "https://researchr.org/publication/Harper85" cites: 0 citedby: 0 pages: "21-30" booktitle: "pos" kind: "inproceedings" key: "Harper85" - title: "Canonicity for 2-dimensional type theory" author: - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2012" doi: "http://doi.acm.org/10.1145/2103656.2103697" links: doi: "http://doi.acm.org/10.1145/2103656.2103697" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/LicataH12" researchr: "https://researchr.org/publication/LicataH12" cites: 0 citedby: 0 pages: "337-348" booktitle: "POPL" kind: "inproceedings" key: "LicataH12" - title: "Constructing Type Systems over an Operational Semantics" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "1992" abstract: "Type theories in the sense of Martin-Löf and the NuPRL system are based on taking as primitive a type-free programming language given by an operational semantics, and defining types as partial equivalence relations on the set of closed terms. The construction of a type system is based on a general form of inductive definition that may either be taken as acceptable in its own right, or further explicated in terms of other patterns of induction. One such account, based on a general theory of inductively-defined relations, was given by Allen. An alternative account, based on an essentially set-theoretic argument, is presented. " tags: - "programming languages" - "semantics" - "rule-based" - "pattern language" - "type system" - "programming" - "operational semantics" - "type theory" researchr: "https://researchr.org/publication/Harper92" cites: 0 citedby: 0 journal: "JSC" volume: "14" number: "1" pages: "71-84" kind: "article" key: "Harper92" - title: "Persistent triangulations Journal of Functional Programming" author: - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Hal Burch" link: "https://researchr.org/alias/hal-burch" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Gary L. Miller" link: "https://researchr.org/alias/gary-l.-miller" - name: "Noel Walkington" link: "https://researchr.org/alias/noel-walkington" year: "2001" tags: - "persistent" - "functional programming" - "programming" researchr: "https://researchr.org/publication/BlellochBCHMW01" cites: 0 citedby: 0 journal: "JFP" volume: "11" number: "5" pages: "441-466" kind: "article" key: "BlellochBCHMW01" - title: "Homotopical patch theory" author: - name: "Carlo Angiuli" link: "https://researchr.org/alias/carlo-angiuli" - name: "Edward Morehouse" link: "https://researchr.org/alias/edward-morehouse" - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2014" doi: "http://doi.acm.org/10.1145/2628136.2628158" links: doi: "http://doi.acm.org/10.1145/2628136.2628158" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/AngiuliMLH14" researchr: "https://researchr.org/publication/AngiuliMLH14" cites: 0 citedby: 0 pages: "243-256" booktitle: "ICFP" kind: "inproceedings" key: "AngiuliMLH14" - title: "Signatures for a Network Protocol Stack: A Systems Application of Standard ML" author: - name: "Edoardo Biagioni" link: "https://researchr.org/alias/edoardo-biagioni" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" - name: "Brian Milnes" link: "https://researchr.org/alias/brian-milnes" year: "1994" doi: "http://doi.acm.org/10.1145/182409.182431" links: doi: "http://doi.acm.org/10.1145/182409.182431" tags: - "protocol" researchr: "https://researchr.org/publication/BiagioniHLM94" cites: 0 citedby: 0 pages: "55-64" booktitle: "lfp" kind: "inproceedings" key: "BiagioniHLM94" - title: "Operational Interpretations of an Extension of F::omega:: with Control Operators" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Mark Lillibridge" link: "https://researchr.org/alias/mark-lillibridge" year: "1996" researchr: "https://researchr.org/publication/HarperL96%3A0" cites: 0 citedby: 0 journal: "JFP" volume: "6" number: "3" pages: "393-417" kind: "article" key: "HarperL96:0" - title: "Robin Milner 1934--2010: verification, languages, and concurrency" author: - name: "Andrew D. Gordon" link: "https://researchr.org/alias/andrew-d.-gordon" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "John Harrison" link: "https://researchr.org/alias/john-harrison" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" - name: "Peter Sewell" link: "https://researchr.org/alias/peter-sewell" year: "2011" doi: "http://doi.acm.org/10.1145/1926385.1926439" links: doi: "http://doi.acm.org/10.1145/1926385.1926439" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/GordonHHJS11" researchr: "https://researchr.org/publication/GordonHHJS11" cites: 0 citedby: 0 pages: "473-474" booktitle: "POPL" kind: "inproceedings" key: "GordonHHJS11" - title: "A Type-Theoretic Approach to Higher-Order Modules with Sharing" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Mark Lillibridge" link: "https://researchr.org/alias/mark-lillibridge" year: "1994" tags: - "systematic-approach" researchr: "https://researchr.org/publication/HarperL94" cites: 0 citedby: 0 pages: "123-137" booktitle: "POPL" kind: "inproceedings" key: "HarperL94" - title: "Parametricity and Variants of Girard s ::::J:::: Operator" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "John C. Mitchell" link: "https://researchr.org/alias/john-c.-mitchell" year: "1999" doi: "http://dx.doi.org/10.1016/S0020-0190(99)00036-8" links: doi: "http://dx.doi.org/10.1016/S0020-0190(99)00036-8" tags: - "C++" researchr: "https://researchr.org/publication/HarperM99" cites: 0 citedby: 0 journal: "ipl" volume: "70" number: "1" pages: "1-5" kind: "article" key: "HarperM99" - title: "Deciding Type Equivalence with Singleton Kinds" author: - name: "Christopher A. Stone" link: "https://researchr.org/alias/christopher-a.-stone" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2000" doi: "http://doi.acm.org/10.1145/325694.325724" links: doi: "http://doi.acm.org/10.1145/325694.325724" researchr: "https://researchr.org/publication/StoneH00" cites: 0 citedby: 0 pages: "214-227" booktitle: "POPL" kind: "inproceedings" key: "StoneH00" - title: "A type-theoretic interpretation of standard ML" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Christopher A. Stone" link: "https://researchr.org/alias/christopher-a.-stone" year: "2000" researchr: "https://researchr.org/publication/HarperS00" cites: 0 citedby: 0 pages: "341-388" booktitle: "BIRTHDAY" kind: "inproceedings" key: "HarperS00" - title: "A Type Discipline for Program Modules" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Robin Milner" link: "https://researchr.org/alias/robin-milner" - name: "Mads Tofte" link: "https://researchr.org/alias/mads-tofte" year: "1987" researchr: "https://researchr.org/publication/HarperMT87" cites: 0 citedby: 0 pages: "308-319" booktitle: "tapsoft" kind: "inproceedings" key: "HarperMT87" - title: "An experimental analysis of self-adjusting computation" author: - name: "Umut A. Acar" link: "https://researchr.org/alias/umut-a.-acar" - name: "Guy E. Blelloch" link: "https://researchr.org/alias/guy-e.-blelloch" - name: "Matthias Blume" link: "https://researchr.org/alias/matthias-blume" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Kanat Tangwongsan" link: "https://researchr.org/alias/kanat-tangwongsan" year: "2009" doi: "http://doi.acm.org/10.1145/1596527.1596530" links: doi: "http://doi.acm.org/10.1145/1596527.1596530" tags: - "analysis" researchr: "https://researchr.org/publication/AcarBBHT09" cites: 0 citedby: 0 journal: "TOPLAS" volume: "32" number: "1" kind: "article" key: "AcarBBHT09" - title: "Explicit Polymorphism and CPS Conversion" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Mark Lillibridge" link: "https://researchr.org/alias/mark-lillibridge" year: "1993" researchr: "https://researchr.org/publication/HarperL93" cites: 0 citedby: 0 pages: "206-219" booktitle: "POPL" kind: "inproceedings" key: "HarperL93" - title: "Generational Stack Collection and Profile-Driven Pretenuring" author: - name: "Perry Cheng" link: "https://researchr.org/alias/perry-cheng" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1998" researchr: "https://researchr.org/publication/ChengHL98" cites: 0 citedby: 0 pages: "162-173" booktitle: "PLDI" kind: "inproceedings" key: "ChengHL98" - title: "Mechanizing metatheory in a logical framework" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Daniel R. Licata" link: "https://researchr.org/alias/daniel-r.-licata" year: "2007" doi: "http://dx.doi.org/10.1017/S0956796807006430" links: doi: "http://dx.doi.org/10.1017/S0956796807006430" tags: - "metatheory" researchr: "https://researchr.org/publication/HarperL07" cites: 0 citedby: 0 journal: "JFP" volume: "17" number: "4-5" pages: "613-673" kind: "article" key: "HarperL07" - title: "Higher-order abstract syntax: setting the record straight" author: - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2006" doi: "http://doi.acm.org/10.1145/1165555.1165572" links: doi: "http://doi.acm.org/10.1145/1165555.1165572" tags: - "abstract syntax" researchr: "https://researchr.org/publication/CraryH06" cites: 0 citedby: 0 journal: "sigact" volume: "37" number: "3" pages: "93-96" kind: "article" key: "CraryH06" - title: "Extensional equivalence and singleton types" author: - name: "Christopher A. Stone" link: "https://researchr.org/alias/christopher-a.-stone" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" year: "2006" doi: "http://doi.acm.org/10.1145/1183278.1183281" links: doi: "http://doi.acm.org/10.1145/1183278.1183281" researchr: "https://researchr.org/publication/StoneH06" cites: 0 citedby: 0 journal: "tocl" volume: "7" number: "4" pages: "676-722" kind: "article" key: "StoneH06" - title: "Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers" year: "2001" researchr: "https://researchr.org/publication/tic%3A2000" cites: 0 citedby: 0 booktitle: "Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers" editor: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" volume: "2071" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-42196-3" kind: "proceedings" key: "tic:2000" - title: "Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), Philadelphia, Pennsylvania, May 24-26, 1996" year: "1996" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/1996" researchr: "https://researchr.org/publication/icfp-1996" cites: 0 citedby: 0 booktitle: "Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), Philadelphia, Pennsylvania, May 24-26, 1996" conference: "ICFP" editor: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Richard L. Wexelblat" link: "https://researchr.org/alias/richard-l.-wexelblat" publisher: "ACM" isbn: "0-89791-770-7" kind: "proceedings" key: "icfp-1996"