Parameterized Verification of π-Calculus Systems

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/11691372_3 ◽

2006 ◽

pp. 42-57 ◽

Cited By ~ 5

Author(s):

Ping Yang ◽

Samik Basu ◽

C. R. Ramakrishnan

Keyword(s):

Parameterized Verification ◽

Π Calculus

Download Full-text

Parameterized verification of open procedural programs

Proceedings of the Fifth Balkan Conference in Informatics on - BCI '12 ◽

10.1145/2371316.2371352 ◽

2012 ◽

Author(s):

Aleksandar S. Dimovski

Keyword(s):

Parameterized Verification

Download Full-text

An Automatic Proving Approach to Parameterized Verification

ACM Transactions on Computational Logic ◽

10.1145/3232164 ◽

2018 ◽

Vol 19 (4) ◽

pp. 1-25 ◽

Cited By ~ 3

Author(s):

Yongjian Li ◽

Kaiqiang Duan ◽

David N. Jansen ◽

Jun Pang ◽

Lijun Zhang ◽

...

Keyword(s):

Parameterized Verification

Download Full-text

On Polymorphic Sessions and Functions

ACM Transactions on Programming Languages and Systems ◽

10.1145/3457884 ◽

2021 ◽

Vol 43 (2) ◽

pp. 1-55

Author(s):

Bernardo Toninho ◽

Nobuko Yoshida

Keyword(s):

Natural Deduction ◽

Sequent Calculus ◽

Linear Logic ◽

Linear Formulation ◽

Session Types ◽

Logical Foundation ◽

Π Calculus ◽

Soundness And Completeness ◽

System F ◽

Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Download Full-text