Searcharxiv⌕ Search

arXiv subjects

Robert Harper

Publications and source records attributed to Robert Harper.

36 records · Page 2Linked to original sources
arXiv2020

Cost-Aware Type Theory

Although computational complexity is a fundamental aspect of program behavior, it is often at odds with common type theoretic principles such as function extensionality, which identifies all functions with the same $\textit{input-output}$ behavior. We present a computational type theory called $\mathbf{CATT}$ that has a primitive notion of cost (the number of evaluation steps). We introduce a new dependent function type "funtime" whose semantics can be viewed as a cost-aware version of function extensionality. We prove a collection of lemmas for $\mathbf{CATT}$, including a novel introduction rule for the new funtime type. $\mathbf{CATT}$ can be simultaneously viewed as a framework for analyzing computational complexity of programs and as the beginnings of a semantic foundation for characterizing feasible mathematical proofs.

cs.PL↗
arXiv2019

Parametric Cubical Type Theory

We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and distinctions between the two along the way. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic types, including functions between higher inductive types, and we show by example how relativity can be used to characterize the relational interpretation of inductive types.

cs.LO↗
arXiv2018

A Separation Logic for Concurrent Randomized Programs

We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.

cs.PL↗
arXiv2018

Computational Higher Type Theory IV: Inductive Types

This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of indexed cubical inductive types whose constructors may take dimension parameters and have a specified boundary. Using this schema, we are able to specify and implement many of the higher inductive types which have been postulated in homotopy type theory, including homotopy pushouts, the torus, $W$-quotients, truncations, arbitrary localizations. By including indexed inductive types, we enable the definition of identity types. The addition of higher inductive types makes computational higher type theory a model of homotopy type theory, capable of interpreting almost all of the constructions in the HoTT Book (with the exception of inductive-inductive types). This is the first such model with an explicit canonicity theorem, which specifies the canonical values of higher inductive types and confirms that every term in an inductive type evaluates to such a value.

cs.LO↗
arXiv2018

Competitive Parallelism: Getting Your Priorities Right

Multi-threaded programs have traditionally fallen into one of two domains: cooperative and competitive. These two domains have traditionally remained mostly disjoint, with cooperative threading used for increasing throughput in compute-intensive applications such as scientific workloads and cooperative threading used for increasing responsiveness in interactive applications such as GUIs and games. As multicore hardware becomes increasingly mainstream, there is a need for bridging these two disjoint worlds, because many applications mix interaction and computation and would benefit from both cooperative and competitive threading. In this paper, we present techniques for programming and reasoning about parallel interactive applications that can use both cooperative and competitive threading. Our techniques enable the programmer to write rich parallel interactive programs by creating and synchronizing with threads as needed, and by assigning threads user-defined and partially ordered priorities. To ensure important responsiveness properties, we present a modal type system analogous to S4 modal logic that precludes low-priority threads from delaying high-priority threads, thereby statically preventing a crucial set of priority-inversion bugs. We then present a cost model that allows reasoning about responsiveness and completion time of well-typed programs. The cost model extends the traditional work-span model for cooperative threading to account for competitive scheduling decisions needed to ensure responsiveness. Finally, we show that our proposed techniques are realistic by implementing them as an extension to the Standard ML language.

cs.PL↗
arXiv2018

The RedPRL Proof Assistant (Invited Paper)

RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.

cs.LO↗
arXiv2018

Guarded Computational Type Theory

Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has been difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a hierarchy of universes. We present an operational account of guarded dependent type theory with clocks called Guarded Computational Type Theory, featuring a novel clock intersection connective that enjoys the clock irrelevance principle, as well as a predicative hierarchy of universes which does not require any indexing in clock contexts. Guarded Computational Type Theory is simultaneously a programming language with a rich specification logic, as well as a computational metalanguage that can be used to develop semantics of other languages and logics.

cs.LO↗
arXiv2018

Inferring the time-varying functional connectivity of large-scale computer networks from emitted events

We consider the problem of inferring the functional connectivity of a large-scale computer network from sparse time series of events emitted by its nodes. We do so under the following three domain-specific constraints: (a) non-stationarity of the functional connectivity due to unknown temporal changes in the network, (b) sparsity of the time-series of events that limits the effectiveness of classical correlation-based analysis, and (c) lack of an explicit model describing how events propagate through the network. Under the assumption that the probability of two nodes being functionally connected correlates with the mean delay between their respective events, we develop an inference method whose output is an undirected weighted network where the weight of an edge between two nodes denotes the probability of these nodes being functionally connected. Using a combination of windowing and convolution to calculate at each time window a score quantifying the likelihood of a pair of nodes emitting events in quick succession, we develop a model of time-varying connectivity whose parameters are determined by maximising the model's predictive power from one time window to the next. To assess the effectiveness of our inference method, we construct synthetic data for which ground truth is available and use these data to benchmark our approach against three state-of-the-art inference methods. We conclude by discussing its application to data from a real-world large-scale computer network.

cs.LG↗
arXiv2017

Computational Higher Type Theory III: Univalent Universes and Exact Equality

This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype universes. As in Parts I and II, the main result is a canonicity theorem stating that closed terms of boolean type evaluate to either true or false. This establishes the computational interpretation of Cartesian cubical higher type theory based on cubical programs equipped with a deterministic operational semantics.

cs.LO↗
arXiv2017

Computational Higher Type Theory II: Dependent Cubical Realizability

This is the second in a series of papers extending Martin-Lö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. We define identification types, which classify identifications (paths) in a type, and dependent function and pair types. The main result is a canonicity theorem, which states that a closed term of boolean type evaluates to either true or false. This result establishes the first computational interpretation of higher dependent type theory by giving a deterministic operational semantics for its programs, including operations that realize the Kan condition.

cs.LO↗
arXiv2017

Algebraic Foundations of Proof Refinement

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.

cs.LO↗
arXiv2017

A Higher-Order Logic for Concurrent Termination-Preserving Refinement

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. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.

cs.PL↗
arXiv2016

Computational Higher Type Theory I: Abstract Cubical Realizability

Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf'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. The explanation is extended to incomplete (open) programs by functionality: types and elements must respect equality in their free variables. Equality is evidence-free---two types or elements are at most equal---and equal things are implicitly interchangeable in all contexts. Higher-dimensional type theory extends type theory to account for identifications of types and elements. An identification witnesses that two types or elements are explicitly interchangeable in all contexts by an explicit transport, or coercion, operation. There must be sufficiently many identifications, which is ensured by imposing a generalized form of the Kan condition from homotopy theory. Here we provide a Martin-Löf-style meaning explanation of simple higher-dimensional type theory based on a programming language that includes Kan-like constructs witnessing the computational meaning of the higher structure of types. The treatment includes an example of a higher inductive type (namely, the 1-dimensional sphere) and an example of Voevodsky's univalence principle, which identifies equivalent types. The main result is a computational canonicity theorem that validates the computational interpretation: a closed boolean expression must always evaluate to a boolean value, even in the presence of higher-dimensional structure. This provides the first fully computational formulation of higher-dimensional type theory.

cs.LO↗
arXiv2015

A Note on the Uniform Kan Condition in Nominal Cubical Sets

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. This characterization is used to give a formulation of uniform Kan fibrations in which uniformity emerges as naturality in the additional dimensions.

math.LO↗
arXiv2011

Selective Memoization

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. We describe our approach in the context of a functional language called MFL and an implementation as a Standard ML library. The MFL language employs a modal type system to enable the programmer to express programs that reveal their true data dependences when executed. We prove that the MFL language is sound by showing that that MFL programs yield the same result as they would with respect to a standard, non-memoizing semantics. The SML implementation cannot support the modal type system of MFL statically but instead employs run-time checks to ensure correct usage of primitives.

cs.PL↗
arXiv2010

A Monadic Formalization of ML5

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. This translation both explains the existing ML5 design and suggests some simplifications and generalizations. We have formalized our translation within the Agda proof assistant. Rather than formalizing lax S5 as a proof theory, we \emph{embed} it as a universe within the the dependently typed host language, with the universe elimination given by implementing the modal logic's Kripke semantics. This representation technique saves us the work of defining a proof theory for the logic and proving it correct, and additionally allows us to inherit the equational theory of the meta-language, which can be exploited in proving that the semantics validates the operational semantics of ML5.

cs.PL↗
arXiv2001

On Equivalence and Canonical Forms in the LF Type Theory

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. Neither approach appears to scale well to richer languages with unit types or subtyping, and neither directly addresses the problem of conversion to canonical. In this paper we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages, and yields a new notion of canonical form sufficient for adequate encodings of logical systems. The algorithm is proved complete by a Kripke-style logical relations argument similar to that suggested by Coquand. Crucially, both the algorithm itself and the logical relations rely only on the shapes of types, ignoring dependencies on terms.

cs.LO↗