Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic

2007 ◽  
pp. 163-177 ◽  
Author(s):  
Marcelo P. Fiore
Keyword(s):  
Linear Logic ◽  
Differential Structure ◽  
Intuitionistic Linear Logic

scholarly journals Relating Categorical Semantics for Intuitionistic Linear Logic

2005 ◽  
Vol 13 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Maria Emilia Maietti ◽  
Paola Maneggia ◽  
Valeria de Paiva ◽  
Eike Ritter
Keyword(s):  
Linear Logic ◽  
Categorical Semantics ◽  
Intuitionistic Linear Logic

The finite model property for knotted extensions of propositional linear logic

2005 ◽  
Vol 70 (1) ◽  
pp. 84-98 ◽  
Author(s):  
C. J. van Alten
Keyword(s):  
Linear Logic ◽  
Finite Model ◽  
Algebraic Semantics ◽  
Structural Rule ◽  
Model Property ◽  
Algebraic Models ◽  
Finite Model Property ◽  
Finite Embeddability Property ◽  
Full Algebra ◽  
Intuitionistic Linear Logic

AbstractThe logics considered here are the propositional Linear Logic and propositional Intuitionistic Linear Logic extended by a knotted structural rule: . It is proved that the class of algebraic models for such a logic has the finite embeddability property, meaning that every finite partial subalgebra of an algebra in the class can be embedded into a finite full algebra in the class. It follows that each such logic has the finite model property with respect to its algebraic semantics and hence that the logic is decidable.

scholarly journals Reconciling Lambek’s restriction, cut-elimination and substitution in the presence of exponential modalities

2020 ◽  
Vol 30 (1) ◽  
pp. 239-256 ◽  
Author(s):  
Max Kanovich ◽  
Stepan Kuznetsov ◽  
Andre Scedrov
Keyword(s):  
Linear Logic ◽  
Cut Elimination ◽  
Lambek Calculus ◽  
Full Extent ◽  
Intuitionistic Linear Logic

Abstract The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek’s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek’s restriction and cut elimination and another system with Lambek’s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek’s restriction is folklore and known to be undecidable.

Girard translation and logical predicates

2000 ◽  
Vol 10 (1) ◽  
pp. 77-89 ◽  
Author(s):  
MASAHITO HASEGAWA
Keyword(s):  
Short Proof ◽  
Linear Logic ◽  
Lambda Calculus ◽  
Independent Interest ◽  
Proof Technique ◽  
Typed Lambda Calculus ◽  
Intuitionistic Linear Logic

We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this paper can be read as a tutorial on this proof technique for reasoning about relations between type theories.

scholarly journals Syntactic soundness proof of a type-and-capability system with hidden state

2012 ◽  
Vol 23 (1) ◽  
pp. 38-144 ◽  
Author(s):  
FRANÇOIS POTTIER
Keyword(s):  
Linear Logic ◽  
Scale Up ◽  
Type System ◽  
The Other ◽  
Formal Definition ◽  
Proof Technique ◽  
The Core ◽  
Proof Techniques ◽  
Definition Of ◽  
Intuitionistic Linear Logic

AbstractThis paper presents a formal definition and machine-checked soundness proof for a very expressive type-and-capability system, that is, a low-level type system that keeps precise track of ownership and side effects. The programming language has first-class functions and references. The type system's features include the following: universal, existential, and recursive types; subtyping; a distinction between affine and unrestricted data; support for strong updates; support for naming values and heap fragments via singleton and group regions; a distinction between ordinary values (which exist at runtime) and capabilities (which do not); support for dynamic reorganizations of the ownership hierarchy by disassembling and reassembling capabilities; and support for temporarily or permanently hiding a capability via frame and anti-frame rules. One contribution of the paper is the definition of the type-and-capability system itself. We present the system as modularly as possible. In particular, at the core of the system, the treatment of affinity, in the style of dual intuitionistic linear logic, is formulated in terms of an arbitrarymonotonic separation algebra, a novel axiomatization of resources, ownership, and the manner in which they evolve with time. Only the peripheral layers of the system are aware that we are dealing with a specific monotonic separation algebra, whose resources are references and regions. This semi-abstract organization should facilitate further extensions of the system with new forms of resources. The other main contribution is a machine-checked proof of type soundness. The proof is carried out in the Wright and Felleisen's syntactic style. This offers an evidence that this relatively simple-minded proof technique can scale up to systems of this complexity, and constitutes a viable alternative to more sophisticated semantic proof techniques. We do not claim that the syntactic technique is superior: We simply illustrate how it is used and highlight its strengths and shortcomings.

Sign in / Sign up

Export Citation Format

Share Document