In a previous work with Antonio Bucciarelli, we introduced indexed linear logic as a tool for studying and enlarging the denotational semantics of linear logic. In particular, we showed how to define new denotational models of linear logic using symmetric product phase models of indexed linear logic. We present here a strict extension of indexed linear logic for which symmetric product phase spaces provide a complete semantics. We study the connection between this new system and indexed linear logic.

We relate two sequential models of PCF: the sequential algorithm model due to Berry and Curien and the strongly stable model due to Bucciarelli and the author. More precisely, we show that all the morphisms araising in the strongly stable model of PCF are sequential in the sense that they are the “extensional projections” of some sequential algorithms. We define a model of PCF where morphisms are “extensional” sequential algorithms and prove that any equation between PCF terms which holds in (...) this model also holds in the strongly stable model. (shrink)

Linear Logic is a branch of proof theory which provides refined tools for the study of the computational aspects of proofs. These tools include a duality-based categorical semantics, an intrinsic graphical representation of proofs, the introduction of well-behaved non-commutative logical connectives, and the concepts of polarity and focalisation. These various aspects are illustrated here through introductory tutorials as well as more specialised contributions, with a particular emphasis on applications to computer science: denotational semantics, lambda-calculus, logic programming and concurrency theory. The (...) volume is rounded-off by two invited contributions on new topics rooted in recent developments of linear logic. The book derives from a summer school that was the climax of the EU Training and Mobility of Researchers project 'Linear Logic in Computer Science'. It is an excellent introduction to some of the most active research topics in the area. (shrink)

We extend to the exponential connectives of linear logic the study initiated in Bucciarelli and Ehrhard 247). We define an indexed version of propositional linear logic and provide a sequent calculus for this system. To a formula A of indexed linear logic, we associate an underlying formula of linear logic, and a family A of elements of , the interpretation of in the category of sets and relations. Then A is provable in indexed linear logic iff the family A (...) is contained in the interpretation of some proof of . We extend to this setting the product phase semantics of indexed multiplicative additive linear logic introduced in Bucciarelli and Ehrhard , defining the symmetric product phase spaces. We prove a soundness result for this truth-value semantics and show how a denotational model of linear logic can be associated to any symmetric product phase space. Considering a particular symmetric product phase space, we obtain a new coherence space model of linear logic, which is non-uniform in the sense that the interpretation of a proof of !A−B contains informations about the behavior of this proof when applied to “chimeric” arguments of type A . In this coherence semantics, an element of a web can be strictly coherent with itself, or two distinct elements can be “neutral”. (shrink)

We study the notion of logical relation in the coherence space semantics of multiplicative-additive linear logic . We show that, when the ground-type logical relation is “closed under restrictions”, the logical relation associated to any type can be seen as a map associating facts of a phase space to families of points of the web of the corresponding coherence space. We introduce a sequent calculus extension of whose formulae denote these families of points. This logic admits a truth-value semantics in (...) the previously mentioned phase space, and this truth-value semantics faithfully describes the logical relation model we started from. Then we generalize this notion of phase space, we prove a truth-value completeness result for and we derive from any phase model of a denotational model for . Using the truth-value completeness result, we obtain a weak denotational completeness result based on this new denotational semantics. (shrink)

In this paper, we present a categorical model for Multiplicative Additive Polarized Linear Logic , which is the linear fragment of Olivier Laurent’s Polarized Linear Logic. Our model is based on an adjunction between reflective/coreflective full subcategories / of an ambient *-autonomous category . Similar structures were first introduced by M. Barr in the late 1970’s in abstract duality theory and more recently in work on game semantics for linear logic. The paper has two goals: to discuss concrete models and (...) to present various completeness theorems.As concrete examples, we present a hypercoherence model, using Ehrhard’s hereditary/anti-hereditary objects, a Chu-space model, a double gluing model over our categorical framework, and a model based on iterated double gluing over a *-autonomous category.For the multiplicative fragment of. (shrink)

We consider a notion of sequential functional of finite type, more generous than the familiar notion embodied in Plotkin's language PCF. We study both the “full” and “effective” partial type structures arising from this notion of sequentiality. The full type structure coincides with that given by the strongly stable model of Bucciarelli and Ehrhard; it has also been characterized by van Oosten in terms of realizability over a certain combinatory algebra. We survey and relate several known characterizations of these (...) type structures, and obtain some new ones. We show that every finite type can be obtained as a retract of the pure type , and hence that all elements of the effective type structure are definable in PCF extended by a certain universal functional H. We also consider the relationship between our notion of sequentially computable functional and other known notions of higher-type computability. (shrink)

Russkiĭ proekt novoĭ religii -- Istoki novoĭ dukhovnosti -- Bogi Cerebri︠a︡nogo veka -- Religii︠a︡ i revoli︠u︡t︠s︡ii︠a︡ -- Personalii.

We prove a full completeness theorem for multiplicative–additive linear logic using a double gluing construction applied to Ehrhard’s *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free proof. Our proof consists of three steps. We show:• Dinatural transformations on this category satisfy Joyal’s softness property for products and coproducts.• Softness, together with multiplicative full completeness, guarantees (...) that every dinatural transformation corresponds to a Girard proof-structure.• The proof-structure associated with any dinatural transformation is a proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures.The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences. (shrink)

This work offers a new theory of what it means to be a legal person and suggests that it is best understood as a cluster property. The book explores the origins of legal personhood, the issues afflicting a traditional understanding of the concept, and the numerous debates surrounding the topic.

The apology to the reader -- The corpus chair and oxford jurisprudence as evolved by 1952 -- The gladsome light of philosophical jurisprudence -- The elusive sources of Hart's ideas in The Concept of Law -- Cyclops, hedgehogs, and foxes -- Where Homer nodded? -- Judging a pioneer.

Amidst all the anticipation, anxiety, and hype swirling around the year 2000, we may find ourselves searching for some sure guidance as we enter the new millennium. Dharma: The Way of Transcendence provides it. Written by His Divine Grace A. C. Bhaktivedanta Swami Prabhupada, whom scholars and spiritual leaders worldwide recognize as the most distinguished teacher of Indian culture and philosophy of the modern age, Dharma answers essential questions thoughtful people ask in every millenium: Who am I? What are my (...) deepest needs? How can I fulfill them? Srila Prabhupada writes, "The body and the mind are but superfluous outer coverings of the spirit soul. The spirit soul's needs must be fulfilled. The need of the spirit soul is that he wants to get out of the limited sphere of material bondage and fulfill his desire for complete freedom. He wants to get out of the covered walls of the greater universe. He wants to see the free light and the spirit." To learn what that free light and spirit are, and how you can see them, read Dharma. Book jacket. (shrink)

Exploring history pertinent to evolutionary developmental biology (hereafter, Evo-devo) is an exciting prospect given its current status as a cutting-edge field of research. The first and obvious question concerns where to begin searching for materials and sources. Since this new discipline adopts a moniker that intentionally juxtaposes ‘evolution’ and development’, individuals, disciplines, and institutional contexts relevant to the history of evolutionary studies and investigations of ontogeny prompt themselves. Each of these topics has received attention from historians and thus there is (...) both primary and secondary material from which to draw. For example, many historians have documented the historical trajectories of genetics and embryology, their split, and various relations (or lack thereof), especially in the first three decades of the 20th century. (shrink)

A pIausibicRi2;if not self-cvidcntRi2;Ri2;hypoth@sis readily comes to mind: when 0nc tries t0 understand oncsclf, that is, when 0nc works at building a self-image, cme talkx t0 07i656% A stronger formulation of this hypothesis could bc that the more one talks to oneself to construct a self-image, the more this image will gain coherence and sophistication. A corrclational study is presented in which the existence of a relation between thc complexity (or richness) of thc seIfRi2;concept and a more or less frequent (...) use of seifRi2;taik is examined. The results are preliminary because scifRi2;taIk was measured with 21 pilotdnvcntory and the complexity of thc self-concept was scored using a new system. For a detailed discussion of thc role played by self-talk in the acquisition 0f sclfdnformation and its organisation into a seIfRi2;conccpt, scc.. (shrink)

Open peer commentary on the target article “From Objects to Processes: A Proposal to Rewrite Radical Constructivism” by Siegfried J. Schmidt > Upshot: Radical Constructivism should be strictly process-oriented to avoid hidden ontology. S. J. Schmidt provides such a strict process-orientation from a very philosophical viewpoint that, however, still lacks access to empirical research. The purpose of this commentary is to show a way to apply Schmidt’s philosophical framework to empirical research.

PAMVEC is a novel vehicle modeling tool designed to complement the capabilities of dynamic vehicle simulators and be better-suited to the purposes of vehicle technology assessment. This paper presents a validation of PAMVEC against published data for a range of production and pre-production prototype vehicles whose powertrain technologies span the range currently being exhibited by automotive manufacturers. For each vehicle, the PAMVEC model was used to predict the fuel/energy consumption and required peak powertrain output due to acceleration performance. Errors typically.

Lee A. McBride III articulates an ethical position that takes critical pragmatism and Harrisian insurrectionist philosophy seriously. It suggests that there are values and norms that create boundaries that confine, reduce and circumscribe the actions we allow ourselves to consider. This book argues that an insurrectionist ethos is integral in the disavowing of norms and traditions that justify or perpetuate oppression and that we must throw our faith behind something, some set of values, if we want a chance at shaping (...) a future. (shrink)