# Robert Harper - Carnegie Mellon University

## Contact Details

NameRobert Harper |
||

AffiliationCarnegie Mellon University |
||

CityPittsburgh |
||

CountryUnited States |
||

## Pubs By Year |
||

## Pub CategoriesComputer Science - Logic in Computer Science (7) Computer Science - Programming Languages (4) Mathematics - Category Theory (1) Mathematics - Logic (1) |

## Publications Authored By Robert Harper

We contribute a general apparatus for dependent tactic-based proof refinement in the LCF tradition, in which the statements of subgoals may express a dependency on the proofs of other subgoals; this form of dependency is extremely useful and can serve as an algorithmic alternative to extensions of LCF based on non-local instantiation of schematic variables. Additionally, we introduce a novel behavioral distinction between refinement rules and tactics based on naturality. Our framework, called Dependent LCF, is already deployed in the nascent RedPRL proof assistant for computational cubical type theory. Read More

Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. Read More

This is the second in a series of papers extending Martin-L\"{o}f's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I, and extend it to a meaning explanation of dependent higher-dimensional type theory. This extension requires generalizing the computational Kan condition given in Part I, and considering the action of type families on paths. Read More

Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-L\"of's meaning explanations for constructive type theory define the concept of a type in terms of computation. Briefly, a type is a complete (closed) program that evaluates to a canonical type whose members are complete programs that evaluate to canonical elements of that type. Read More

Bezem, Coquand, and Huber have recently given a constructively valid model of higher type theory in a category of nominal cubical sets satisfying a novel condition, called the uniform Kan condition (UKC), which generalizes the standard cubical Kan condition (as considered by, for example, Williamson in his survey of combinatorial homotopy theory) to admit phantom "additional" dimensions in open boxes. This note, which represents the authors' attempts to fill in the details of the UKC, is intended for newcomers to the field who may appreciate a more explicit formulation and development of the main ideas. The crux of the exposition is an analogue of the Yoneda Lemma for co-sieves that relates geometric open boxes bijectively to their algebraic counterparts, much as its progenitor for representables relates geometric cubes to their algebraic counterparts in a cubical set. Read More

This paper presents language techniques for applying memoization selectively. The techniques provide programmer control over equality, space usage, and identification of precise dependences so that memoization can be applied according to the needs of an application. Two key properties of the approach are that it accepts and efficient implementation and yields programs whose performance can be analyzed using standard analysis techniques. Read More

**Affiliations:**

^{1}Carnegie Mellon University,

^{2}Carnegie Mellon University

ML5 is a programming language for spatially distributed computing, based on a Curry-Howard correspondence with the modal logic S5. Despite being designed by a correspondence with S5 modal logic, the ML5 programming language differs from the logic in several ways. In this paper, we explain these discrepancies between ML5 and S5 by translating ML5 into a slightly different logic: intuitionistic S5 extended with a lax modality that encapsulates effectful computations in a monad. Read More

This article responds to a critique of higher-order abstract syntax appearing in Logic Column 14, ``Nominal Logic and Abstract Syntax'', cs.LO/0511025. Read More

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality are based on a confluent, strongly-normalizing notion of reduction. Coquand has considered a different approach, directly proving the correctness of a practical equivalance algorithm based on the shape of terms. Read More