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 Tools annual

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 Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Type refinements combine the compositionality of typechecking with theexpressivity of program logics, offering a synergistic approach to programverification. In this paper we apply dependent type refinements to SAX, afutures-based process calculus that arises from the Curry-Howard interpretationof the intuitionistic semi-axiomatic sequent calculus and includes unrestrictedrecursion both at the level of types and processes. With our type refinementsystem, we can reason about the partial correctness of SAX programs,complementing prior work on sized type refinements that supports reasoningabout termination. Our design regime synthesizes the infinitary proof theory ofSAX with that of bidirectional typing and Hoare logic, deriving some standardreasoning principles for data and (co)recursion while enabling informationhiding for codata. We prove syntactic type soundness, which entails a notion ofpartial correctness that respects codata encapsulation. We illustrate ourlanguage through a few simple examples.

Dependent Type Refinements for Futures