The following pages link to Robert Harper (Q724929):
Displayed 50 items.
- Exception tracking in an open world (Q724930) (← links)
- Type checking with universes (Q1177937) (← links)
- Constructing type systems over an operational semantics (Q1199709) (← links)
- Structured theory presentations and logic representations (Q1326777) (← links)
- A simplified account of polymorphic references (Q1334643) (← links)
- A note on ``A simplified account of polymorphic references'' (Q1350743) (← links)
- Automatic generation of staged geometric predicates (Q1426869) (← links)
- Corrigendum: Polymorphic type assignment and CPS conversion (Q1426870) (← links)
- Parametricity and variants of Girard's \(J\) operator (Q1606917) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- Verified tail bounds for randomized programs (Q1791202) (← links)
- Relational interpretations of recursive types in an operational setting. (Q1854316) (← links)
- (Q2704327) (← links)
- On the Unusual Effectiveness of Logic in Computer Science (Q2736585) (← links)
- Persistent triangulations (Q2757100) (← links)
- Practical Foundations for Programming Languages (Q2805272) (← links)
- Homotopical patch theory (Q2819684) (← links)
- Syntactic Logical Relations for Polymorphic and Recursive Types (Q2864153) (← links)
- A universe of binding and computation (Q2936809) (← links)
- Canonicity for 2-dimensional type theory (Q2942884) (← links)
- A type theory for memory allocation and data layout (Q2942924) (← links)
- A type system for higher-order modules (Q2942929) (← links)
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement (Q2988673) (← links)
- Space profiling for parallel functional programs (Q3021408) (← links)
- Modular type classes (Q3189786) (← links)
- Towards a mechanized metatheory of standard ML (Q3189797) (← links)
- (Q3204067) (← links)
- A framework for defining logics (Q4033837) (← links)
- (Q4222944) (← links)
- (Q4364397) (← links)
- A module system for a programming language based on the LF logical framework (Q4399511) (← links)
- (Q4420573) (← links)
- (Q4721631) (← links)
- Proof-directed debugging (Q4943360) (← links)
- Syntax and models of Cartesian cubical type theory (Q5022926) (← links)
- (Q5028425) (← links)
- Logical Relations as Types: Proof-Relevant Parametricity for Program Modules (Q5056429) (← links)
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (Q5079726) (← links)
- Logic representation in LF (Q5096264) (← links)
- Guarded Computational Type Theory (Q5145367) (← links)
- A dependently typed assembly language (Q5178007) (← links)
- Automatic generation of staged geometric predicates (Q5178011) (← links)
- Space profiling for parallel functional programs (Q5178766) (← links)
- Deciding type equivalence in a language with singleton kinds (Q5178854) (← links)
- Adaptive functional programming (Q5178910) (← links)
- On equivalence and canonical forms in the LF type theory (Q5277716) (← links)
- Extensional equivalence and singleton types (Q5277760) (← links)
- Mechanizing metatheory in a logical framework (Q5308093) (← links)
- Computational higher-dimensional type theory (Q5370902) (← links)
- Parallel functional arrays (Q5370905) (← links)