A Concurrent Model for Linear Logic | Zendy

Emmanuel Beffara | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Concurrent Model for Linear Logic

Author(s) -

Emmanuel Beffara

Publication year - 2006

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.11.055

Subject(s) - realizability , linear logic , intuitionistic logic , curry–howard correspondence , modal logic , computer science , mathematical proof , programming language , linear temporal logic , normal modal logic , semantics (computer science) , interpretation (philosophy) , calculus (dental) , kripke semantics , intermediate logic , theoretical computer science , modal , algebra over a field , mathematics , natural deduction , description logic , pure mathematics , medicine , chemistry , geometry , dentistry , polymer chemistry

International audienceWe build a realizability model for linear logic using a name-passing process calculus. The construction is based on testing semantics for processes, drawing ideas from spatial and modal logics, and yields a new type system for process calculi that ensures termination while allowing significantly concurrent behaviours. Then we study how embeddings of intuitionistic and classical logics into linear logic induce typed translations of lambda and lambda-mu calculi in which new concurrent instructions can be introduced, thus sketching the basis for a Curry-Howard interpretation of linear and classical proofs in terms of concurrent interaction

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research