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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Classical (or Boolean) type theory is the type theory that allows the typeinference $\sigma \to \bot) \to \bot => \sigma$ (the type counterpart ofdouble-negation elimination), where $\sigma$ is any type and $\bot$ isabsurdity type. This paper first presents a denotational semantics for asimplified version of Parigot's lambda-mu calculus, a premier example ofclassical type theory. In this semantics the domain of each type is dividedinto infinitely many ranks and contains not only the usual members of the typeat rank 0 but also their negative, conjunctive, and disjunctive shadows in thehigher ranks, which form an infinitely nested Boolean structure. Absurdity type$\bot$ is identified as the type of truth values. The paper then presents a newdeduction system of classical type theory, a sequent calculus called theclassical type system (CTS), which involves the standard logical operators suchas negation, conjunction, and disjunction and thus reflects the discussedsemantic structure in a more straightforward fashion.

Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory