Related papers: Cost-Aware Type Theory
We present $\textbf{calf}$, a $\textbf{c}$ost-$\textbf{a}$ware $\textbf{l}$ogical $\textbf{f}$ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of…
A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input, and then to compute a closed-form upper bound on that recurrence. We give…
The theory of computational complexity focuses on functions and, hence, studies programs whose interactive behavior is reduced to a simple question/answer pattern. We propose a broader theory whose ultimate goal is expressing and analyzing…
A central method for analyzing the asymptotic complexity of a functional program is to extract and then solve a recurrence that expresses evaluation cost in terms of input size. The relevant notion of input size is often specific to a…
Complexity remains one of the central challenges in science and technology. Although several approaches at defining and/or quantifying complexity have been proposed, at some point each of them seems to run into intrinsic limitations or…
We study a cost-aware programming language for higher-order recursion dubbed $\textbf{PCF}_\mathsf{cost}$ in the setting of synthetic domain theory (SDT). Our main contribution relates the denotational cost semantics of…
We present Decalf, a directed, effectful cost-aware logical framework for studying quantitative aspects of functional programs with effects. Like Calf, the language is based on an internal phase distinction between the behavior of a program…
We study the problem of automatically computing the time complexity of concurrent object-oriented programs. To determine this complexity we use intermediate abstract descriptions that record relevant information for the time analysis (cost…
The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural…
This paper proposes a model of decision-making under uncertainty in which an agent is constrained in her cognitive ability to consider complex acts. We identify the complexity of an act according to the corresponding partition of state…
We introduce a notion of complexity of diagrams (and in particular of objects and morphisms) in an arbitrary category, as well as a notion of complexity of functors between categories equipped with complexity functions. We discuss several…
We present a new method for inferring complexity properties for a class of programs in the form of flowcharts annotated with loop information. Specifically, our method can (soundly and completely) decide if computed values are polynomially…
In the original work on the cost-aware logical framework by Niu et al., a dependent variant of the call-by-push-value language for cost analysis, the authors conjectured that the canonicity property of the type theory can be succinctly…
Cost functions provide a framework for constructions of sets Turing below the halting problem that are close to computable. We carry out a systematic study of cost functions. We relate their algebraic properties to their expressive…
In quantitative program analysis, values are assigned to execution traces to represent a quality measure. Such analyses cover important applications, e.g. resource usage. Examining all traces is well known to be intractable and therefore…
We present two metalanguages for developing $\textit{synthetic cost-aware denotational semantics}$ of programming languages. Extending the recent work of Niu et al. [2022] on $\textbf{calf}$, a dependent type theory for both cost and…
Classical complexity theory measures the cost of computing a function, but many computational tasks require committing to one valid output among several. We introduce determination depth -- the minimum number of sequential layers of…
Inductive concept learning is the task of learning to assign cases to a discrete set of classes. In real-world applications of concept learning, there are many different types of cost involved. The majority of the machine learning…
We start by an introduction to the basic concepts of computability theory and the introduction of the concept of Turing machine and computation universality. Then se turn to the exploration of trade-offs between different measures of…
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,…