Hostname: page-component-8448b6f56d-sxzjt Total loading time: 0 Render date: 2024-04-23T13:21:21.575Z Has data issue: false hasContentIssue false
  • English
  • Français

Relating reasoning methodologies in linear logic and process algebra

Published online by Cambridge University Press:  10 November 2014

YUXIN DENG ,
ROBERT J. SIMMONS  and
ILIANO CERVESATO
YUXIN DENG
Affiliation:
Department of Computer Science and Engineering, Shanghai Jiao Tong University, 800 Dongchuan Road, Shanghai 200240, China Email: yuxindeng@sjtu.edu.cn
ROBERT J. SIMMONS
Affiliation:
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A. Email: rjsimmon@cs.cmu.edu
ILIANO CERVESATO
Affiliation:
Carnegie Mellon University, Qatar campus, Qatar Email: iliano@cmu.edu
Get access Rights & Permissions [Opens in a new window]

Abstract

We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of barbed preorder for a CCS-like process calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely simulation and labelled transition systems. This result establishes a connection between an approach to reason about process specifications, the barbed preorder, and a method to reason about logic specifications, the logical preorder.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Issue 5 , June 2016 , pp. 868 - 906
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. (1994) Proofs as processes. Theoretical Computer Science 135 5–9.CrossRefGoogle Scholar
Amadio, R., Castellani, I. and Sangiorgi, D. (1998). On bisimulation for the asynchronous pi-calculus. Theoretical Computer Science 195 (2)291–324.CrossRefGoogle Scholar
Barber, A. (1996) Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, Laboratory for Foundations of Computer Sciences, University of Edinburgh.Google Scholar
Caires, L. and Cardelli, L. (2003) A spatial logic for concurrency (part I). Information and Computation 186 (2)194–235.CrossRefGoogle Scholar
Caires, L. and Pfenning, F. (2010) Session types as intuitionistic linear propositions. In: Proceedings of the 21st International Conference on Concurrency Theory. Springer Lecture Notes in Computer Science 6269 222–236.CrossRefGoogle Scholar
Caires, L., Pfenning, F. and Toninho, B. (2012) Towards concurrent type theory. In: Proceedings of the Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, ACM 1–12.Google Scholar
Cervesato, I., Durgin, N., Kanovich, M. I. and Scedrov, A. (2000) Interpreting strands in linear logic. In: Veith, H., Heintze, N. and Clark, E. (eds.) Workshop on Formal Methods and Computer Security – FMCS'00, Chicago, IL.Google Scholar
Cervesato, I., Pfenning, F., Walker, D. and Watkins, K. (2002) A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-2002-002, Department of Computer Science, Carnegie Mellon University. Revised May 2003.Google Scholar
Cervesato, I. and Scedrov, A. (2009) Relating state-based and process-based concurrency through linear logic. Information and Computation 207 1044–1077.CrossRefGoogle Scholar
Dam, M. (1994) Process-algebraic interpretations of positive linear and relevant logics. Journal of Logic and Computation 4 (6)939–973.CrossRefGoogle Scholar
Deng, Y. and Du, W. (2011) Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical Report CMU-CS-11-110, Carnegie Mellon University.Google Scholar
Deng, Y. and Hennessy, M. (2011) On the semantics of markov automata. In: Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP'11) Springer Lecture Notes in Computer Science 6756 307–318.CrossRefGoogle Scholar
Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C. and Zhang, C. (2007) Characterising testing preorders for finite probabilistic processes. In: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society 313–325.Google Scholar
Ehrhard, T. and Laurent, O. (2010) Interpreting a finitary pi-calculus in differential interaction nets. Information and Computation 208 (6)606–633.CrossRefGoogle Scholar
Fournet, C. and Gonthier, G. (2000) The join calculus: A language for distributed mobile programming. Applied Semantics Summer School – APPSEM'00, Caminha. Available at http://research.microsoft.com/~fournet.Google Scholar
Fournet, C. and Gonthier, G. (2005) A hierarchy of equivalences for asynchronous calculi. Journal of Logic and Algebraic Programming 63 (1)131–173.CrossRefGoogle Scholar
Gentzen, G. (1935) Untersuchungen über das logische schließen. I. Mathematische Zeitschrift 39 (1)176–210.CrossRefGoogle Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Girard, J.-Y., Taylor, P. and Lafont, Y. (1989) Proofs and Types, Cambridge University Press.Google Scholar
Hennessy, M. and Milner, R. (1985) Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32 (1)137–161.CrossRefGoogle Scholar
Hoare, C. (1985) Communicating Sequential Processes, Prentice Hall.Google Scholar
Honda, K. and Yoshida, N. (1995) On reduction-based process semantics. Theoretical Computer Science 151 (2)437–486.CrossRefGoogle Scholar
Lincoln, P. and Saraswat, V. (1991) Proofs as concurrent processes: A logical interpretation for concurrent constraint programming. Technical report, Systems Sciences Laboratory, Xerox PARC.Google Scholar
Martin-Löf, P. (1996) On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1 (1)11–60.Google Scholar
McDowell, R., Miller, D. and Palamidessi, C. (2003) Encoding transition systems in sequent calculus. Theoretical Computer Science 294 (3)411–437.CrossRefGoogle Scholar
Miller, D. (1992) The π-calculus as a theory in linear logic: Preliminary results. In: Lamma, E. and Mello, P. (eds.) Proceedings of the Workshop on Extensions to Logic Programming – ELP'92. Springer-Verlag Lecture Notes in Computer Science 660 242–265.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency, Prentice Hall.Google Scholar
Pfenning, F. (2000) Structural cut elimination I. Intuitionistic and classical logic. Information and Computation 157 (1/2)84–141.CrossRefGoogle Scholar
Pfenning, F. and Davies, R. (2001) A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11 (4)511–540. Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999.CrossRefGoogle Scholar
Rathke, J. and Sobocinski, P. (2008) Deriving structural labelled transitions for mobile ambients. In: Proceedings of the 19th International Conference on Concurrency Theory. Springer Lecture Notes in Computer Science 5201 462–476.CrossRefGoogle Scholar
Sangiorgi, D. and Walker, D. (2001) The π-Calculus: A Theory of Mobile Processes, Cambridge University Press.Google Scholar
Tiu, A. and Miller, D. (2004) A proof search specification of the π-calculus. In: 3rd Workshop on the Foundations of Global Ubiquitous Computing. Electronic Notes in Theoretical Computer Science 138 79–101.CrossRefGoogle Scholar
Wadler, P. (2012) Propositions as sessions. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ACM 273–286.CrossRefGoogle Scholar