Bard Bloom
ABSTRACT
We propose a general definition of higher-order process calculi, generalizing CHOCS [Tho89] and related calculi, and investigate its basic properties. We give sufficient conditions under which a calculus is finitely-branching and effective. We show that a suitable notion of higher-order bisimulation is a congruence for a subclass of higher-order calculi. We illustrate our definitions with a simple calculus strictly stronger than CHOCS.
- Ace92.Luca Aceto. Eliminating junk rules from GSOS languages. (Unpublished note; to appear, probably as part of something else.), July 1992.Google Scholar
- BC90.Kenneth Birman and Robert Cooper. The Isis project: Real experience with a fault tolerant programming system. Technical Report 90-i138, Department of Computer Science, Cornell University, July 1990.Google ScholarCross Ref
- BCG91.Kenneth P. Birman, Robert Cooper, and Barry Gleeson. Programming with process groups: Group and multicast semantics. Technical Report 91-1185, Department of Computer Science, Cornell University, January 1991.Google Scholar
- BIM88.Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced (preliminary report). In Conference Record o)" the Fifteenth Annual A CM Symposium on Principles of Programming Languages, pages 229-239, 1988. Also appears as MIT Technical Memo MIT/LCS/TM-345. Google ScholarDigital Library
- Blo89.Bard Bloom. Ready Simulation, Bisimulation, and the Semantics of CCS-Like Languages. PhD thesis, Massachusetts Institute of Technology, August 1989.Google Scholar
- Hen93.Matthew Hennessy. A fully abstract denotational model for higher-order processes (extended abstract). In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 397-408. IEEE Computer Society Press, 1993. (Full version in Sussex TR 6/92).Google ScholarCross Ref
- Mil91.Robin Milner. The polyadic ~-calculus" A tutorial. In Proc. International Summer School on Logic an dAlgebra of Specification. Marktoberdorf, 1991.Google Scholar
- MPW92.Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes I and II. Information and Computation, 100:1-40 and 41-77, 1992. Google ScholarDigital Library
- Rep89.John H. Reppy. First-class synchronous operations in Standard ML. Technical Report 89-1068, Department of Computer Science, Cornell University, December 1989. Google ScholarDigital Library
- Rep91.John H. Reppy. CML" A higher-order concurrent language. SIGPLAN Notices, 26(6)'293-305, June t991. Google ScholarDigital Library
- Tho89.Bent Thomsen. A calculus of higher order communicating systems. In Conference Record of the Sixteenth Annual A CM Symposium on Principles of Programming Languages, pages 142-154, 1989. Google ScholarDigital Library
- Vaa93.Frits Vaandrager. Expressiveness results for process algebras. In de Bakker, de Roever, and Rozenberg, editors, Semantics" Foundations and Applications, pages 609-620. Springer-Verlag, 1993. LNCS 666. Also appears as CWI Tech Report CS-R9301. Google ScholarDigital Library
Index Terms
- CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms (preliminary report)
Recommendations
On generic context lemmas for higher-order calculi with sharing
This paper proves several generic variants of context lemmas and thus contributes to improving the tools for observational semantics of deterministic and non-deterministic higher-order calculi that use a small-step reduction semantics. The generic (...
I-terms in ordered resolution and superposition calculi: retrieving lost completeness
AISC'10/MKM'10/Calculemus'10: Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematicsOrdered resolution and superposition are the state-of-the-art proof procedures used in saturation-based theorem proving, for non equational and equational clause sets respectively. In this paper, we present extensions of these calculi that permit one to ...
Higher-order abstract syntax in classical higher-order logic
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and PracticeHigher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to ...
Comments