Source author record

Daniel R. Licata

Daniel R. Licata appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Programming Languages math.AT math.LO Logic in Computer Science math.CT

Catalog footprint

What is connected

6works

5topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

Denotational semantics as a foundation for cost recurrence extraction for functional languages

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 a formal account of that method for functional programs in a higher-order language with let-polymorphism. The method consists of two phases. In the first phase, a monadic translation is performed to extract a cost-annotated version of the original program. In the second phase, the extracted program is interpreted in a model. The key feature of this second phase is that different models describe different notions of size. This plays out in several ways. For example, when analyzing functions that take arguments of inductive types, different notions of size may be appropriate depending on the analysis. When analyzing polymorphic functions, our approach shows that one can formally describe the notion of size of an argument in terms of the data that is common to the notions of size for each type instance of the domain type. We give several examples of different models that formally justify various informal cost analyses to show the applicability of our approach.

preprint2021arXiv

Synthetic Spectra via a Monadic and Comonadic Modality

We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a more intricate judgemental structure than previous modal extensions of Homotopy Type Theory. We use this theory to develop an synthetic approach to spectra, where spectra are represented by certain types, and constructions on them by type structure: maps of spectra by ordinary functions, loop spaces by the identity type, and so on. We augment the type theory with a pair of axioms, one which implies that the spectra are stable, and the other which relates synthetic spectra to the ordinary definition of spectra in type theory as $Ω$-spectra. Finally, we show that the type theory is sound and complete for an abstract categorical semantics, in terms of a category-with-families with a weak endomorphism whose functor on contexts is a bireflection, i.e. has a counit an a unit that are a section-retraction pair.

preprint2020arXiv

Denotational recurrence extraction for amortized analysis

A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the banker's method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees.

preprint2015arXiv

Denotational cost semantics for functional languages with inductive types

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 datatype, with measures including the length of a list, the maximum element in a list, and the height of a tree. In this work, we give a formal account of the extraction of cost and size recurrences from higher-order functional programs over inductive datatypes. Our approach allows a wide range of programmer-specified notions of size, and ensures that the extracted recurrences correctly predict evaluation cost. To extract a recurrence from a program, we first make costs explicit by applying a monadic translation from the source language to a complexity language, and then abstract datatype values as sizes. Size abstraction can be done semantically, working in models of the complexity language, or syntactically, by adding rules to a preorder judgement. We give several different models of the complexity language, which support different notions of size. Additionally, we prove by a logical relations argument that recurrences extracted by this process are upper bounds for evaluation cost; the proof is entirely syntactic and therefore applies to all of the models we consider.

preprint2013arXiv

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The category theory and homotopy theory suggest new principles to add to type theory, and type theory can be used in novel ways to formalize these areas of mathematics. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Though simple, this example is interesting for several reasons: it illustrates the new principles in homotopy type theory; it mixes ideas from traditional homotopy-theoretic proofs of the result with type-theoretic inductive reasoning; and it provides a context for understanding an existing puzzle in type theory---that a universe (type of types) is necessary to prove that the constructors of inductive types are disjoint and injective.

preprint2010arXiv

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.