Directory of Proofs as Processes Resources

Home > Science > Math > Logic and Foundations > Computational Logic > Combinatory Logic and Lambda Calculus > Formulae-as-Types Correspondence > Proofs as Processes

Applications of logic to process algebras are often inspired by the concurrent analogue of the formulae-as-types correspondence proposed by Samson Abramsky and inspired by Girard's linear logic.

Resources in This Category

• A Non Functional Calculus: Linear Logic and Concurrency (2000)

  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.3024
  (CiteSeer) This paper proposes the *-calculus as an approach that unifies Abramsky's proofs-as-processes approach with Boudol and Berry's Chemical Abstract Machine approach.

• Completeness Results for Linear Logic on Petri Nets (1993)

  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.1293
  (CiteSeer) Article by Engberg and Winskel showing that Petri nets provide a class of model for linear logic that is complete.

• The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes (1998)

  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.8118
  (CiteSeer) This PhD thesis proposes the fusion calculus as a simplified pi-calculus with many formal advantages.

 

Home > Science > Math > Logic and Foundations > Computational Logic > Combinatory Logic and Lambda Calculus > Formulae-as-Types Correspondence > Proofs as Processes

 

---

 

Thanks to DMOZ, which built a great web directory for nearly two decades and freely shared it with the web. About us