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

Dynamically typed object-oriented languages enable programmers to writeelegant, reusable and extensible programs. However, with the currentmethodology for program verification, the absence of static type informationcreates significant overhead. Our proposal is two-fold:  First, we propose a layer of abstraction hiding the complexity of dynamictyping when provided with sufficient type information. Since this essentiallycreates the illusion of verifying a statically-typed program, the effortrequired is equivalent to the statically-typed case.  Second, we show how the required type information can be efficiently derivedfor all type-safe programs by integrating a type inference algorithm into Hoarelogic, yielding a semi-automatic procedure allowing the user to focus on thosetyping problems really requiring his attention. While applying type inferenceto dynamically typed programs is a well-established method by now, our approachcomplements conventional soft typing systems by offering formal proof as athird option besides modifying the program (static typing) and accepting thepresence of runtime type errors (dynamic typing).

Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic -- Extended Version --