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 introduce an extension of first-order logic that comes equipped withadditional predicates for reasoning about an abstract state. Sequents in thelogic comprise a main formula together with pre- and postconditions in thestyle of Hoare logic, and the axioms and rules of the logic ensure that theassertions about the state compose in the correct way. The main result of thepaper is a realizability interpretation of our logic that extracts programsinto a mixed functional/imperative language. All programs expressible in thislanguage act on the state in a sequential manner, and we make this intuitionprecise by interpreting them in a semantic metatheory using the state monad.Our basic framework is very general, and our intention is that it can beinstantiated and extended in a variety of different ways. We outline in detailone such extension: A monadic version of Heyting arithmetic with a wellfoundedwhile rule, and conclude by outlining several other directions for future work.

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language