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

In this paper we consider a type system with a universal type $\omega$ whereany term (whether open or closed, $\beta$-normalising or not) has type$\omega$. We provide this type system with a realisability semantics where anatomic type is interpreted as the set of $\lambda$-terms saturated by a certainrelation. The variation of the saturation relation gives a number ofinterpretations to each type. We show the soundness and completeness of oursemantics and that for different notions of saturation (based on weak headreduction and normal $\beta$-reduction) we obtain the same interpretation fortypes. Since the presence of $\omega$ prevents typability and realisabilityfrom coinciding and creates extra difficulties in characterizing theinterpretation of a type, we define a class ${\mathbb U}^+$ of the so-calledpositive types (where $\omega$ can only occur at specific positions). We showthat if a term inhabits a positive type, then this term is $\beta$-normalisableand reduces to a closed term. In other words, positive types can be used torepresent abstract data types. The completeness theorem for ${\mathbb U}^+$becomes interesting indeed since it establishes a perfect equivalence betweentypable terms and terms that inhabit a type. In other words, typability andrealisability coincide on ${\mathbb U}^+$. We give a number of examples toexplain the intuition behind the definition of ${\mathbb U}^+$ and to show thatthis class cannot be extended while keeping its desired properties.

A completeness result for a realisability semantics for an intersection type system