On phase semantics and denotational semantics: The exponentials
An indexed version of propositional linear logic with exponentials is defined together with a sequent calculus for this system. To a formula \(A\) of indexed linear logic are associated: an underlying formula \(\underline{A}\) of linear logic, an interpretation \(|\underline{A}|\) of this formula in the category of sets and relations, and a family \(\langle A\rangle\) of elements of \(A\). Then \(A\) is provable in indexed linear logic iff the family \(\langle A\rangle\) is contained in the interpretation of some proof of \(\underline{A}\). To this setting the product phase semantics of indexed multiplicative additive linear logic (by the same authors) is extended (symmetric product phase spaces are defined). A soundness result is proved and it is shown how a denotational model of linear logic can be associated to any symmetric product phase space. On this basis a new coherence space model of linear logic is obtained. NEWLINENEWLINENEWLINESome details to give an idea how indexed linear logic \(\text{LL}(I)\) is defined. NEWLINENEWLINENEWLINELet \(I\) be an infinite denumerable set. NEWLINENEWLINENEWLINELet \(J, K\) be two sets. A function \(u:J\rightarrow K\) is almost injective if, for any \(k\in K\), the set \(u^{-1}(k)\) is finite. NEWLINENEWLINENEWLINEEvery formula \(A\) has a domain \(d(A)\subseteq I\). (\dots) NEWLINENEWLINENEWLINEIf \(A, B\) are formulae of a domain \(J\subseteq I\) then \(A\otimes B\) is a formula of the domain \(J\). (Similarly for \(par\).) NEWLINENEWLINENEWLINEIf \(A\) is a formula of a domain \(J\) and \(B\) is a formula of a domain \(K\), \(J\cap K=\emptyset\), then \(A\oplus B, A\& B\) are formulae of the domain \(J+K\) (the disjoint union of \(J\) and \(K\)). NEWLINENEWLINENEWLINEIf \(A\) is a formula of a domain \(J\) and \(u:J\rightarrow K\) is an almost injective function then \(!_uA\) and \(?_uA\) are formulae of the domain \(K\) (\dots)NEWLINENEWLINENEWLINEFor \(\text{LL}(I)\) a succedent-only sequent calculus is considered.
- A completeness theorem for symmetric product phase spaces
- On phase semantics and denotational semantics in multiplicative-additive linear logic
- Stratified coherence spaces: A denotational semantics for light linear logic
- An Indexed System for Multiplicative Additive Polarized Linear Logic
- scientific article; zbMATH DE number 1231516
- A completeness theorem for symmetric product phase spaces
- scientific article; zbMATH DE number 2185654 (Why is no real title available?)
- scientific article; zbMATH DE number 431771 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1229489 (Why is no real title available?)
- scientific article; zbMATH DE number 1231467 (Why is no real title available?)
- scientific article; zbMATH DE number 512784 (Why is no real title available?)
- scientific article; zbMATH DE number 786485 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- Kripke logical relations and PCF
- Linear logic
- On phase semantics and denotational semantics in multiplicative-additive linear logic
- The finite model property for various fragments of linear logic
- Relational model of second order linear logic
- On phase semantics and denotational semantics in multiplicative-additive linear logic
- The bang calculus revisited
- Non-idempotent intersection types in logical form
- Generalized bounded linear logic and its categorical semantics
- The spirit of node replication
- Non-uniform hypercoherences
- Non-uniform (hyper/multi)coherence spaces
- A General Class of Models of $\mathcal{H}^*$
- An Indexed System for Multiplicative Additive Polarized Linear Logic
- Visible acyclic differential nets. I: Semantics
- The Scott model of linear logic is the extensional collapse of its relational model
- Execution time of λ-terms via denotational semantics and intersection types
- scientific article; zbMATH DE number 7003195 (Why is no real title available?)
- A \(\mathsf{MALL}\) geometry of interaction based on indexed linear logic
- The bang calculus and the two Girard's translations
- Towards a semantic measure of the execution time in call-by-value lambda-calculus
- Differentials and distances in probabilistic coherence spaces
- Tight typings and split bounds, fully developed
- A completeness theorem for symmetric product phase spaces
- scientific article; zbMATH DE number 7756108 (Why is no real title available?)
- The bang calculus revisited
- Coherent differentiation
- Relational Models for the Lambek Calculus with Intersection and Constants
- Node Replication: Theory And Practice
- Profinite lambda-terms and parametricity
- A deep quantitative type system
- Semantic bounds and multi types, revisited
- Unifying graded linear logic and differential operators
- Coherent Taylor expansion as a bimonad
- From differential linear logic to coherent differentiation
- Uniformity and the Taylor expansion of ordinary lambda-terms
This page was built for publication: On phase semantics and denotational semantics: The exponentials
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5939845)
