English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present ${\bf decalf}$, a ${\bf d}$irected, ${\bf e}$ffectful ${\bfc}$ost-${\bf a}$ware ${\bf l}$ogical ${\bf f}$ramework for studyingquantitative aspects of functional programs with effects. Like ${\bf calf}$,the language is based on a formal phase distinction between the extension andthe intension of a program, its pure behavior as distinct from its costmeasured by an effectful step-counting primitive. The type theory ensures thatthe behavior is unaffected by the cost accounting. Unlike ${\bf calf}$, thepresent language takes account of effects, such as probabilistic choice andmutable state; this extension requires a reformulation of ${\bf calf}$'sapproach to cost accounting: rather than rely on a "separable" notion of cost,here a cost bound is simply another program. To make this formal, we equipevery type with an intrinsic preorder, relaxing the precise cost accountingintrinsic to a program to a looser but nevertheless informative estimate. Forexample, the cost bound of a probabilistic program is itself a probabilisticprogram that specifies the distribution of costs. This approach serves as astreamlined alternative to the standard method of isolating a recurrence thatbounds the cost in a manner that readily extends to higher-order, effectfulprograms.  The development proceeds by first introducing the ${\bf decalf}$ type system,which is based on an intrinsic ordering among terms that restricts in theextensional phase to extensional equality, but in the intensional phasereflects an approximation of the cost of a program of interest. Thisformulation is then applied to a number of illustrative examples, includingpure and effectful sorting algorithms, simple probabilistic programs, andhigher-order functions. Finally, we justify ${\bf decalf}$ via a model in thetopos of augmented simplicial sets.

Decalf: A Directed, Effectful Cost-Aware Logical Framework