Naoki Kobayashi
- BERGER, M., GAY, S., AND NAGARAJAN, R. 1997. A typed calculus of deadlock-free processes. Draft paper, Imperial College, London.Google Scholar
- COLBY, C. 1995. Analyzing the communication topology of concurrent programs. In Proceedings of the A CM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, New York, 202-213. Google Scholar
- GAY, S. J. 1993. A sort inference algorithm for the polyadic 7r-calculus. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 429-438. Google Scholar
- HODAS, J. S. AND MILLER, D. 1994. Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110, 2, 327-365. Google Scholar
- HONDA, K. AND YOSHIDA, N. 1995. On reduction-based process semantics. Theor. Comput. Sci. 151, 2, 437-486. Google Scholar
- IGARASHI, A. AND KOBAYASHI, N. 1997. Type-based analysis of usage of communication channels for concurrent programming languages. In Proceedings of International Static Analysis Symposium (SAS'97). Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, 187-201. Google Scholar
- KOBAYASHI, N. 1996a. Concurrent linear logic programming. Ph.D. thesis, Dept. of Information Science, Univ. of Tokyo, Japan.Google Scholar
- KOBAYASHI, N. 1996b. A partially deadlock-free typed process calculus (I)--a simple system. Tech. Rep. 96-02, Dept. of Information Science, Univ. of Tokyo, Japan.Google Scholar
- KOBAYASHI, N. AND YONEZAWA, A. 1995. Towards foundations for concurrent object-oriented programming--types and language design. Theory Pract. Object Syst. 1, 4, 243-268. Google Scholar
- KOBAYASHI, N., PIERCE, B. C., AND TURNER, D. N. 1996. Linearity and the pi-calculus. In Proceedings of A CM SIGPLAN/SIGA CT Symposium on Principles of Programming Languages. ACM Press, New York, 358-371. Google Scholar
- MACKIE, I. 1994. Lilac: A functional programming language based on linear logic. J. Funct. Program. 4, 4 (Oct.), 1-39.Google Scholar
- MILNER, R. 1990. Function as processes. In Automata, Language and Programming. Lecture Notes in Computer Science, vol. 443. Springer-Verlag, Berlin, 167-180. Google Scholar
- MILNER, R. 1993. The polyadic 7r-calculus: A tutorial. In Logic and Algebra of Specification, F. L. Bauer, W. Brauer, and H. Schwichtenberg, Eds. Springer-Verlag, Berlin.Google Scholar
- MILNER, R., PARROW, J., AND WALKER, D. 1992. A calculus of mobile processes, I, II. Inf. Comput. 100, 1-77. Google Scholar
- NESTMANN, U. 1997. What is a 'good' encoding of guarded choice? In Proceedings of EXPRESS'97. Electronic Notes in Theoretical Computer Science, vol. 7. Elsevier Science Publishers, Amsterdam.Google Scholar
- NIELSON, H. R. AND NIELSON, F. 1994. Higher-order concurrent programs with finite communication topology. In Proceedings of A CM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 84-97. Google Scholar
- OSTHEIMER, G. AND DAVIE, A. J. T. 1993. 7r-calculus characterizations of some practical A-calculus reduction strategies. Tech. rep., St. Andrews Univ., Scotland.Google Scholar
- OYAMA, Y., TAURA, K., AND YONEZAWA, A. 1997. An efficient compilation framework for languages based on a concurrent process calculus. In Proceedings of Euro-Par '97 Parallel Processing, Object-Oriented Programming. Lecture Notes in Computer Science, vol. 1300. Springer-Verlag, Berlin, 546-553. Google Scholar
- PEYTON JONES, S. 1996. Concurrent Haskell. In Proceedings of A CM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 295-308. Google Scholar
- PIERCE, B. AND SANGIORGI, D. 1993. Typing and subtyping for mobile processes. In Proceedings of IEEE Symposium on Logic in Computer Science. IEEE, New York, 376-385.Google Scholar
- PIERCE, B. C. AND SANGIORGI, D. 1997. Behavioral equivalence in the polymorphic pi-calculus. In Proceedings of A CM SIGPLAN/SIGA CT Symposium on Principles of Programming Languages. ACM Press, New York, 242-255. Google Scholar
- PIERCE, B. C. AND TURNER, D. N. 1995. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming (TPPP). Lecture Notes in Computer Science, vol. 907. Springer-Verlag, Berlin, 187-215. Google Scholar
- PIERCE, B. C. AND TURNER, D. N. 1997. Pict: A programming language based on the pi-calculus. Tech. rep., Computer Science Dept., Indiana Univ. To appear in Milner Festschrift, MIT Press, 1997.Google Scholar
- REPPY, J. H. 1991. CML: A higher-order concurrent language. In Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation. ACM Press, New York, 293-305. Google Scholar
- SANGIORGI, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.Google Scholar
- SANGIORGI, D. 1997. The name discipline of uniform receptiveness (extended abstract). In Proceedings of ICALP'97. Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, Berlin, 303-313. Google Scholar
- SHAPIRO, E. 1989. The family of concurrent logic programming languages. ACM Comput. Surv. 21, 3 (Sept.), 413-510. Google Scholar
- TURNER, D. T. 1996. The polymorphic pi-calculus: Theory and implementation. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.Google Scholar
- VASCONCELOS, V. T. AND HONDA, K. 1993. Principal typing schemes in a polyadic 7r-calculus. In Proceedings of CONCUR'93. Lecture Notes in Computer Science, vol. 715. Springer-Verlag, Berlin, 524-538. Google Scholar
- WALKER, D. 1995. Objects in the 7r-calculus. Inf. Comput. 116, 253-271. Google Scholar
- YONEZAWA, A. AND TOKORO, M. 1987. Object-Oriented Concurrent Programming. The MIT Press, Cambridge, Mass. Google Scholar
- YOSHIDA, N. 1996. Graph types for monadic mobile processes. In Proceedings of FST/TCS'16. Lecture Notes in Computer Science, vol. 1180. Springer-Verlag, Berlin, 371-387. Full version as LFCS report, ECS-LFCS-96-350, Univ. of Edinburgh. Google Scholar
Index Terms
- A partially deadlock-free typed process calculus
Recommendations
An Implicitly-Typed Deadlock-Free Process Calculus
CONCUR '00: Proceedings of the 11th International Conference on Concurrency TheoryWe extend Kobayashi and Sumii's type system for the deadlock-free π-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii's type system helps high-level reasoning about concurrent programs by guaranteeing that communication on ...
A Partially Deadlock-free Typed Process Calculus
LICS '97: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer ScienceWe propose a novel static type system for a process calculus, which ensures both partial deadlock-freedom and partial confluence. The key novel ideas are (1) introduction of the order of channel use as type information, and (2) classification of ...
Typed closure conversion for the calculus of constructions
PLDI '18Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...
Comments