5 found
Order:
  1.  8
    On Phase Semantics and Denotational Semantics in Multiplicative–Additive Linear Logic.Antonio Bucciarelli & Thomas Ehrhard - 2000 - Annals of Pure and Applied Logic 102 (3):247-282.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  2.  14
    On Phase Semantics and Denotational Semantics: The Exponentials.Antonio Bucciarelli & Thomas Ehrhard - 2001 - Annals of Pure and Applied Logic 109 (3):205-241.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  3.  9
    Projecting Sequential Algorithms on Strongly Stable Functions.Thomas Ehrhard - 1996 - Annals of Pure and Applied Logic 77 (3):201-244.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  4
    A Relational Semantics for Parallelism and Non-Determinism in a Functional Setting.Antonio Bucciarelli, Thomas Ehrhard & Giulio Manzonetto - 2012 - Annals of Pure and Applied Logic 163 (7):918-934.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  5.  14
    Linear Logic in Computer Science.Thomas Ehrhard (ed.) - 2004 - Cambridge University Press.
    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 (...)
    Direct download  
     
    Export citation  
     
    Bookmark