Robert Harper
#9,590
Most Influential Person Now
Computer scientist
Robert Harper 's AcademicInfluence.com Rankings
Robert Harper computer-science Degrees
Computer Science
#496
World Rank
#515
Historical Rank
Database
#1821
World Rank
#1909
Historical Rank
Download Badge
Computer Science
Robert Harper 's Degrees
- PhD Computer Science Cornell University
- Bachelors Mathematics Princeton University
Similar Degrees You Can Earn
Why Is Robert Harper Influential?
(Suggest an Edit or Addition)According to Wikipedia, Robert William "Bob" Harper, Jr. is a computer science professor at Carnegie Mellon University who works in programming language research. Prior to his position at Carnegie Mellon, Harper was a research fellow at the University of Edinburgh.
Robert Harper 's Published Works
Published Works
- Definition of standard ML (1990) (2508)
- A framework for defining logics (1993) (1333)
- The Definition of Standard ML (Revised) (1997) (387)
- Compiling polymorphism using intensional type analysis (1995) (348)
- A type-theoretic approach to higher-order modules with sharing (1994) (339)
- Practical Foundations for Programming Languages (2012) (251)
- Typed closure conversion (1996) (211)
- A Language-Based Approach to Security (2001) (200)
- Adaptive functional programming (2002) (199)
- Higher-order modules and the phase distinction (1989) (178)
- TIL: a type-directed, optimizing compiler for ML (2004) (170)
- Typing first-class continuations in ML (1991) (156)
- On the type structure of standard ML (1993) (144)
- The essence of ML (1988) (143)
- Abstract models of memory management (1995) (139)
- What is a recursive module? (1999) (132)
- Towards a mechanized metatheory of standard ML (2007) (130)
- A record calculus based on symmetric concatenation (1991) (119)
- Mechanizing metatheory in a logical framework (2007) (119)
- Generational stack collection and profile-driven pretenuring (1998) (116)
- An experimental analysis of self-adjusting computation (2006) (115)
- On equivalence and canonical forms in the LF type theory (2001) (113)
- A symmetric modal lambda calculus for distributed computing (2004) (113)
- Selective memoization (2003) (110)
- Self-adjusting computation (2004) (108)
- A dependently typed assembly language (2001) (104)
- A type system for higher-order modules (2003) (104)
- On the Unusual Effectiveness of Logic in Computer Science (2001) (103)
- A type-theoretic interpretation of standard ML (2000) (95)
- An effective theory of type refinements (2003) (92)
- A Simplified Account of Polymorphic References (1994) (90)
- The definition of standard ML, Version 3 (1988) (83)
- Dynamizing static algorithms, with applications to dynamic trees and history independence (2004) (81)
- Explicit polymorphism and CPS conversion (1993) (80)
- Type Checking with Universes (1991) (79)
- Introduction to standard ml (1986) (76)
- Polymorphic type assignment and CPS conversion (1993) (74)
- Type-Safe Distributed Programming with ML5 (2007) (74)
- Deciding type equivalence in a language with singleton kinds (2000) (72)
- Signatures for a network protocol stack: a systems application of Standard ML (1994) (65)
- Understanding and evolving the ml module system (2005) (62)
- Modal types for mobile code (2008) (60)
- Structured Theory Presentations and Logic Representations (1994) (59)
- Modular type classes (2007) (57)
- Higher-Order Rewriting with Dependent Types (1999) (53)
- Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures (2009) (53)
- Canonicity for 2-dimensional type theory (2012) (53)
- Space profiling for parallel functional programs (2008) (51)
- Syntactic Logical Relations for Polymorphic and Recursive Types (2007) (49)
- Semantics of memory management for polymorphic languages (1999) (48)
- Extensional equivalence and singleton types (2006) (47)
- Practical Foundations for Programming Languages (2nd. Ed.) (2016) (47)
- An Interpretation of Standard ML in Type Theory (1997) (46)
- Computational higher-dimensional type theory (2017) (46)
- A universe of binding and computation (2009) (45)
- The TIL/ML Compiler: Performance and Safety through Types (1996) (43)
- Proof-directed debugging (1999) (42)
- Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities (2018) (41)
- A type theory for memory allocation and data layout (2003) (41)
- Focusing on Binding and Computation (2008) (41)
- Constructing Type Systems over an Operational Semantics (1992) (40)
- Standard ML: Report ECS-LFCS-86-2 (1986) (40)
- Relational Interpretations of Recursive Types in an Operational Setting (1999) (40)
- A Type Discipline for Program Modules (1987) (37)
- Structure and representation in LF (1989) (36)
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement (2017) (35)
- Higher inductive types in cubical computational type theory (2019) (35)
- 2-Dimensional Directed Type Theory (2011) (34)
- The definition of standard ML Version 2: LFCS report ECS-LFCS-88-62 (1988) (33)
- Homotopical patch theory (2014) (33)
- Trustless Grid Computing in ConCert (2002) (32)
- A Network Protocol Stack in Standard ML (2001) (32)
- A separation logic for concurrent randomized programs (2018) (32)
- A Library for Self-Adjusting Computation (2006) (30)
- Computational Higher Type Theory III: Univalent Universes and Exact Equality (2017) (30)
- A Formulation of Dependent ML with Explicit Equality Proofs (2005) (30)
- Syntax and models of Cartesian cubical type theory (2021) (29)
- A Module System for a Programming Language Based on the LF Logical Framework (1998) (28)
- Distributed Control Flow with Classical Modal Logic (2005) (28)
- Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft) (1989) (27)
- The Fox project : advanced development of systems software (1991) (26)
- Distributed programming with distributed authorization (2010) (25)
- A Type-Theoretic Account of Standard ML 1996 (Version 1). (1996) (25)
- Extensible records without subsumption (1990) (25)
- Advanced Languages for Systems Software: The Fox Project in 1994 (1994) (24)
- Relational Interpretations of Recursive Types in an operational Setting (Summary) (1997) (24)
- Singleton kinds and singleton types (2000) (24)
- Homotopy Type Theory: Univalent Foundations of Mathematics (2013) (23)
- Computational Higher Type Theory I: Abstract Cubical Realizability (2016) (23)
- Automatic Generation of Staged Geometric Predicates (2001) (23)
- Typed compilation of recursive datatypes (2003) (23)
- Implementing the TILT Internal Language (2000) (21)
- Design considerations for ML-style module systems (2005) (21)
- The Fox Project: Advanced Language Technology for Extensible Systems (1998) (21)
- Computational Higher Type Theory IV: Inductive Types (2018) (20)
- Strict bidirectional type checking (2005) (20)
- Parametricity and Variants of Girard's J Operator (1999) (20)
- Cache and I/O efficent functional algorithms (2013) (20)
- A separate compilation extension to standard ML (2006) (19)
- TIL: A Type-Directed Optimizing Compiler (1996) (19)
- Logical Relations as Types: Proof-Relevant Parametricity for Program Modules (2020) (19)
- Cartesian Cubical Type Theory (2017) (18)
- Logic Representation in LF (1989) (18)
- Computational Higher Type Theory II: Dependent Cubical Realizability (2016) (18)
- Programming Languages: Theory and Practice (2005) (17)
- A Note on "A Simplified Account of Polymorphic References" (1996) (17)
- Scalable real-time parallel garbage collection for symmetric multiprocessors (2001) (16)
- Automated techniques for provably safe mobile code (2000) (16)
- Toward a Practical Type Theory for Recursive Modules (2001) (16)
- Programming in Standard ML (2002) (16)
- Positively dependent types (2009) (15)
- Scheduling deterministric parallel programs (2009) (15)
- Principles and a Preliminary Design for ML2000 (2000) (14)
- Using page residency to balance tradeoffs in tracing garbage collection (2005) (14)
- Systems of polymorphic type assignment in LF (1990) (14)
- Incremental Recompilation for Standard ML of New Jersey (1994) (14)
- Internal Parametricity for Cubical Type Theory (2020) (13)
- Competitive parallelism: getting your priorities right (2018) (13)
- Typed Closure Conversion for Recursively-Defined Functions (1998) (13)
- Verified Tail Bounds for Randomized Programs (2018) (12)
- Responsive parallel computation: bridging competitive and cooperative threading (2017) (12)
- Standard ML Signatures for a Protocol Stack (1993) (12)
- Parametric Cubical Type Theory (2019) (11)
- A Compilation Manager for Standard ML of New Jersey (1994) (11)
- Covering Spaces in Homotopy Type Theory (2016) (10)
- Modules and Persistence in Standard ML (1988) (10)
- Guarded Computational Type Theory (2018) (9)
- Homotopical patch theory* (2016) (9)
- Certifying compilation for standard ml in a type analysis framework (2005) (9)
- The RedPRL Proof Assistant (Invited Paper) (2018) (9)
- How to Believe a Twelf Proof (2005) (8)
- Cache efficient functional algorithms (2015) (8)
- A Monadic Formalization of ML5 (2010) (7)
- Higher-order abstract syntax: setting the record straight (2006) (7)
- Operational interpretations of an extension of Fω with control operators (1996) (7)
- Mechanizing the Metatheory of Standard ML ∗ (2006) (7)
- Improved Fault Localization using Transfer Learning and Language Modeling (2020) (7)
- Sheaf semantics of termination-insensitive noninterference (2022) (7)
- Compiling with Non-Parametric Polymorphism (Preliminary Report) (1994) (7)
- Advanced module systems: a guide for the perplexed (abstract of invited talk) (2000) (6)
- Algebraic Foundations of Proof Refinement (2017) (6)
- Correctness of compiling polymorphism to dynamic typing* (2016) (6)
- Inferring Functional Connectivity From Time-Series of Events in Large Scale Network Deployments (2019) (6)
- Persistent triangulations Journal of Functional Programming (2001) (6)
- SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations (2008) (6)
- Logical modeling frameworks for the optimization of discrete-continuous systems (2006) (6)
- A cost-aware logical framework (2021) (5)
- Homotopy type theory: unified foundations of mathematics and computation (2015) (5)
- The semantics of standard LM Version 1: LFCS report ECS-LFCS-87-36 (1987) (5)
- A Method for Temporal Event Correlation (2019) (5)
- Dependntly typed programming with domain-specific logics (2011) (5)
- Commentary on Practical Foundations for Programming Languages (Second Edition) * (2017) (5)
- Network events in a large commercial network: What can we learn? (2018) (5)
- Adaptive Memoization (2003) (5)
- The history of Standard ML (2020) (5)
- Structure and Efficiency of Computer Programs (2014) (5)
- A language for access control (2007) (4)
- An Extensible Theory of Indexed Types (2007) (4)
- A Note on the Uniform Kan Condition in Nominal Cubical Sets (2015) (4)
- The application of Neural Networks to predicting the root cause of service failures (2017) (4)
- Proceedings of the first ACM SIGPLAN international conference on Functional programming (1996) (4)
- Meaning explanations at higher dimension (2018) (4)
- Transparent and Opaque Interpretations of Datatypes (1998) (4)
- Manifest Security for Distributed Information (2006) (3)
- Parallel functional arrays (2017) (3)
- Compiling with Non-Parametric Polymorphism. (1994) (3)
- The Cult of the Bound Variable: The 9 th Annual ICFP Programming Contest (2006) (3)
- Modularity in the LF Logical Framework (1991) (3)
- Deciding Type Equivalence with Singleton Kinds. (2000) (3)
- Implementing Software Architectures in Standard Ml Position Paper (1994) (3)
- Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight (2006) (3)
- Advanced module systems (invited talk): a guide for the perplexed (2000) (3)
- Cookbook, a recipe for fault localization (2018) (3)
- 2-Dimensional Directed Dependent Type Theory (2011) (3)
- Type Refinements (2001) (2)
- Notes on Logical Frameworks (2012) (2)
- ML and beyond (1997) (2)
- A Performance Comparison of Interval Arithmetic and Error Analysis for Geometric Predicates (2000) (2)
- Note on Conditional Compilation in Standard ML (1993) (2)
- An Equational Logical Framework for Type Theories (2021) (2)
- Practical Foundations for Programming Languages: Judgments and Rules (2012) (2)
- Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report (2009) (2)
- Special Issue on ML (1992) (2)
- Mechanizing the meta-theory of programming languages (2005) (2)
- Advanced Languages for Systems Software (1994) (2)
- Towards a Functional Library for Fault-Tolerant Grid Computing (2002) (2)
- Multiscale Scheduling: Integrating Competitive and Cooperative Scheduling in Theory and in Practice (2007) (1)
- Interactive Computation in an Open World (2015) (1)
- A Logical View of Effects (2004) (1)
- A Semantic Framework for Scheduling Parallel Programs (2007) (1)
- ML and beyond (1996) (1)
- Research in programming languages for composability, safety, and performance (1996) (1)
- A Pronominal Approach to Binding and Computation (2009) (1)
- Structure and Efficiency of Computer Programs (2014) (1)
- Self-Adjusting Programming (2005) (1)
- Cost-Aware Type Theory (2020) (1)
- Corrigendum: Polymorphic Type Assignment and CPS Conversion (2003) (1)
- Exactness of the Mayer-Vietoris Sequence in Homotopy Type Theory e cavallo (2015) (1)
- A Modal Language for Effects (2004) (1)
- Homotopical patch theory (2014) (1)
- How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler (1998) (1)
- Refining Objects (2014) (0)
- Type Refinements in an Open World (Extended Abstract) (2015) (0)
- FUNCTIONAL PEARL. Proof-directed debugging – Corrigendum (2009) (0)
- Practical Foundations for Programming Languages: Subtyping (2012) (0)
- Type Refinements for Compiler Correctness (2013) (0)
- Foundations and Applications of Higher-Dimensional Directed Type Theory 1 Overview (2010) (0)
- Persistent Triangulations Guy Blelloch (1999) (0)
- The semantics of standard LM Version 1 (1987) (0)
- PFPL Supplement: How to (Re)Invent Girard’s Method∗ (2018) (0)
- Dynamic Semantics for Modules (1997) (0)
- Appendix: Full Grammar (1997) (0)
- Exception tracking in an open world (2018) (0)
- Computational Higher Type Theory ( CHTT ) (2018) (0)
- Computational Cubical Type Theory (2018) (0)
- Syntax of Modules (1997) (0)
- Standard ML Signatures for a Protocol (1993) (0)
- Tail Bounds for Randomized Programs (2017) (0)
- Compiling with Non-Parametric Polymorphism ( Preliminary Report ) rYTI ( L (0)
- L O ] 2 4 A pr 2 01 8 Guarded Computational Type eory (2018) (0)
- 15 – 212 : Fundamental Structures of Computer Science II Notes on Regular Expression Matching (1997) (0)
- Practical Foundations for Programming Languages: Product Types (2012) (0)
- Practical Foundations for Programming Languages: Hypothetical and General Judgments (2012) (0)
- A Type-Theoretic Interpretation of Standard ML (cid:3) (2001) (0)
- Sheaf semantics of termination-insensitive noninterference: (Extended Version) (2022) (0)
- Short Presentation : Incremental Copying Collection with Pinning ( Progress Report ) (2003) (0)
- λ-Calculus: The Other Turing Machine (2015) (0)
- Modularity Matters Most (2001) (0)
- Foundations of Formal Program Development Other Faculty: Gradute Students: Ergo Report (2009) (0)
- Advanced Language Technology for Extensible Systems (1998) (0)
- Position paper: practical foundations for lrogramming languages (2008) (0)
- Types in compilation : Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000 : revised selected papers (2001) (0)
- λ-Calculus : The Other Turing Machine Guy Blelloch and (2015) (0)
- T H E O R E T I C A L P E A R L S Correctness of Compiling Polymorphism to Dynamic Typing (2015) (0)
- A Monadic Formalization of ML 5 (2015) (0)
- Inferring the time-varying functional connectivity of large-scale computer networks from emitted events (2018) (0)
- Functional Topology Inference from Network Events (2019) (0)
- An Epistemic Formulation of Information Flow Security (2013) (0)
- Structure aid Representation ii-1 LF (1989) (0)
- First-Class Continuations in ML VBruce (0)
- 15–212: Fundamental Structures of Computer Science II Some Notes on Grammars and Parsing (1997) (0)
- Submitted to POPL 2011 2-Dimensional Directed Dependent Type Theory (2010) (0)
- Static Semantics for Modules (1997) (0)
- Practical Foundations for Programming Languages: Hierarchy and Parameterization (2012) (0)
- A metalanguage for cost-aware denotational semantics (2022) (0)
- Enhancements to Language Modeling Techniques for Adaptable Log Message Classification (2022) (0)
- Benchmark Prog. Size (1997) (0)
- 15-399 Supplementary Notes : An Algebraic View of Logic (2005) (0)
- Explorations in the problem of interactive systems design for 'intelligent places' (2005) (0)
- Functional Programming 1 Homotopical Patch Theory (2016) (0)
- AD-A 250 954 onue cec Polymorphic Type Assignment and CPS Conversion (0)
- An Epistemic Formulation of Information Flow Security ( Draft , Under Review ) (2013) (0)
- Practical Foundations for Programming Languages: Inheritance (2012) (0)
- Structure and Eciency of Computer Programs (2014) (0)
- Dynamic Semantics for the Core (1997) (0)
- Appendix: What is New? (1997) (0)
- Hayashi Susumu and Nakano Hiroshi. PX. A computational logic . Foundations of computing. The MIT Press, Cambridge, Mass., and London, 1989, xiv + 200 pp. (1991) (0)
- Practical Foundations for Programming Languages: Type Safety (2012) (0)
- Balancing capacity and epidemic spread in the global airline network (2020) (0)
- Practical Foundations for Programming Languages: Symbol (2012) (0)
- Practical Foundations for Programming Languages: Recursive Types (2012) (0)
- Practical Foundations for Programming Languages: Plotkin's PCF (2012) (0)
- 15 – 212 : Fundamental Structures of Computer Science II Basic Computability Theory (1997) (0)
- Special issue on Logical Frameworks and Metalanguages http//www-sop.inria.fr/certilab/LFM00/cfp-jfp.html (2000) (0)
- A Simplified Account of Polymorphic References. Revised (1993) (0)
- Combining Memoization and Dynamic Dependence Graphs (2004) (0)
- Static Semantics for the Core (1997) (0)
- Cubical Computational Semantics for Higher 1 Inductive Types (2018) (0)
- Semi-Synchronous Conflict Detection Software Development (0)
- Efficient Recursion in the Presence of Effects ∗ (0)
- An overview of the Oregon programming languages summer school (2010) (0)
- An Epistemic Formulation of Information Flow Analysis (2013) (0)
- Syntax of the Core (1997) (0)
- Robin Milner 1934--2010: verification, languages, and concurrency (2011) (0)
- PFPL Supplement: CPS Transformation ∗ (2018) (0)
- The Untyped λ-Calculus (2012) (0)
- Focusing on Computation with Binding (2008) (0)
- Practical Foundations for Programming Languages: Gödel's T (2012) (0)
- 7-23-2014 Structure and Efficiency of Computer Programs (2015) (0)
- Logical Relations as Types (2021) (0)
- Appendix: The Initial Static Basis (1997) (0)
- Appendix: Derived Forms (1997) (0)
- The 9th Annual ICFP Programming Contest (2006) (0)
- Manifest Security (2007) (0)
- Amortized Analysis via Coinduction (2023) (0)
- Residenc y to Balance Tradeoffs in Tracing Garbage Collection (0)
- Exploring the Adaptability of Word Embeddings to Log Message Classification (2021) (0)
- Types for Systems Design : A Position Paper (2003) (0)
- Practical Foundations for Programming Languages: Appendix: Finite Sets and Finite Functions (2012) (0)
- Practical Foundations for Programming Languages: Syntactic Objects (2012) (0)
- 1 Type-Safe Multithreaded Programming with Priorities (2017) (0)
- PFPL Supplement: The Structure of an Interpreter ∗ (2020) (0)
- Appendix: The Initial Dynamic Basis (1997) (0)
- Practical Foundations for Programming Languages: Statics (2012) (0)
- Types in Compilation (2001) (0)
- PFPL Supplement: Automata and Concurrency (2018) (0)
- Type Theory, Computation and Interactive Theorem Proving (2015) (0)
- Kagan, V., Nerode, A. and Subrahmanian, VS., Computing definite logic (1994) (0)
- Scheduling and Space Use in Parallel Functional Programs (2007) (0)
- Practical Foundations for Programming Languages: Abstract Types (2012) (0)
- Algorithmic λ-Calculus for the Design , Analysis , and Implementation of Parallel Algorithms (2016) (0)
- Practical Foundations for Programming Languages: Process Equivalence (2012) (0)
- How Generic is a Generic Back End? Using MLRISC as a Back End for the TIL Compiler (Preliminary Report) (1998) (0)
This paper list is powered by the following services:
Other Resources About Robert Harper
What Schools Are Affiliated With Robert Harper ?
Robert Harper is affiliated with the following schools: