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

Our research is part of a wider project that aims to investigate and reasonabout the correctness of scheme-based source code transformations of Erlangprograms. In order to formally reason about the definition of a programminglanguage and the software built using it, we need a mathematically rigorousdescription of that language.  In this paper, we present our proof-assistant-based formalisation of a subsetof Erlang, intended to serve as a base for proving refactorings correct. Afterdiscussing how we reused concepts from related work, we show the syntax andsemantics of our formal description, including the abstractions involved (e.g.closures). We also present essential properties of the formalisation (e.g.determinism) along with their machine-checked proofs. Finally, we prove thecorrectness of some simple refactoring strategies.

A Proof Assistant Based Formalisation of Core Erlang