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

Session types employ a linear type system that ensures that communicationchannels cannot be implicitly copied or discarded. As a result, manymechanizations of these systems require modeling channel contexts and carefullyensuring that they treat channels linearly. We demonstrate a technique thatlocalizes linearity conditions as additional predicates embedded within typejudgments, which allows us to use structural typing contexts instead of linearones. This technique is especially relevant when leveraging (weak) higher-orderabstract syntax to handle channel mobility and the intricate binding structuresthat arise in session-typed systems. Following this approach, we mechanize asession-typed system based on classical linear logic and its type preservationproof in the proof assistant Beluga, which uses the logical framework LF as itsencoding language. We also prove adequacy for our encoding. This shows thetractability and effectiveness of our approach in modelling substructuralsystems such as session-typed languages.

Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity