Defining concurrent processes constructively. (English) Zbl 0801.68056
Summary: The paper proposes a constructive logic in which a concurrent system can be defined as a proof of a specification. The logic is defined by adding stream types and several rules for them to a simple constructive logic based on intuitionism. The unique feature of the obtained system is in the (MPST) rule, which is a kind of structural induction on streams. The (MPST) rule is based on the idea of Brouwer’s theory of choice sequences in intuitionism and it allows to define a concurrent process, which is actually a Burge’s mapstream function, as a proof of a specification with a good intuition on computation. Several techniques for defining stream- based concurrent programs are also presented through various examples.
MSC:
| 68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03F55 | Intuitionistic mathematics |
Keywords:
formal program development; stream types; constructive logic; intuitionism; concurrent process; stream-based concurrent programsReferences:
| [1] | Aczel, P., Non-well-founded sets, (CSLI Lecture Notes, Vol. 14 (1988), Stanford Univ. Stanford) · Zbl 0668.04001 |
| [2] | Aczel, P.; Mendler, N., A final coalgebra theorem, (Category Theory and Computer Science. Category Theory and Computer Science, Lecture Notes in Computer Science, Vol. 389 (1989), Springer: Springer Berlin) · Zbl 1496.03206 |
| [3] | Beeson, M. J., Foundation of Constructive Mathematics (1985), Springer: Springer Berlin · Zbl 0464.03050 |
| [4] | Burge, W. H., Recursive Programming Techniques (1975), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0321.68002 |
| [5] | Constable, R. L., Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [6] | Dybjer, P.; Sander, H. P., A functional programming approach to the specification and verification of concurrent systems, Formal Aspects of Computing, 1, 303-319 (1989) · Zbl 0694.68015 |
| [7] | Girard, J.-Y., Linear Logic, Theoret. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037 |
| [8] | Goto, S., Proc. Internat. Joint Conf. on Artificial Intelligence, ’85. Proc. Internat. Joint Conf. on Artificial Intelligence, ’85, Concurrency in proof normalization and logic programming (1985) |
| [9] | Hagino, T., A typed lambda calculus with categorical type constructors, (Category Theory and Computer Science. Category Theory and Computer Science, Lecture Notes in Computer Science, Vol. 283 (1987), Springer: Springer Berlin) · Zbl 0643.03010 |
| [10] | Hayashi, S.; Nakano, H., PX: A Computational Logic (1989), MIT Press: MIT Press Cambridge, MA |
| [11] | Howard, W. A., The formulas-as-types notion of construction, (Seldin, J. P.; Hindley, J. R., Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Academic Press: Academic Press New York) |
| [12] | Kahn, G.; MacQueen, D. B., The semantics of a simple language for parallel programming, (Proc. IFIP Congress ’74 (1974), North-Holland: North-Holland Amsterdam) · Zbl 0299.68007 |
| [13] | Kahn, G.; MacQueen, D. B., Coroutine and networks of parallel processes, (Proc. Information Processing ’77 (1977), North-Holland: North-Holland Amsterdam) · Zbl 0363.68076 |
| [14] | Kobayashi, S., Inductive/coinductive definitions and their realizability interpretation (1991), (manuscript) |
| [15] | Martin-Löf, P., Nonstrandard type theory, Proc. Logic Colloquium (1988) |
| [16] | Mendler, N.; Panangaden, P.; Constable, R. L., Infinite objects in type theory, Proc. IEEE Symp. on Logic in Computer Science (1986) |
| [17] | Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008 |
| [18] | Mohring, C., Algorithm development in the calculus of constructions, Proc. IEEE on Logic in Computer Science (1986) |
| [19] | Petersson, K.; Nordström, B.; Smith, J., Programming in Martin-Löf’s Type Theory, An Introduction, (International Series of Monographs on Computer Science, Vol. 7 (1990), Oxford Science Publications: Oxford Science Publications Oxford) · Zbl 0744.03029 |
| [20] | Prawitz, D., Natural Deduction (1965), Almqvist and Wiksell: Almqvist and Wiksell Stockholm · Zbl 0173.00205 |
| [21] | Sato, M., Quty: A concurrent language based on logic and function, (4th Internat. Conf. on Logic Programming (1987), The MIT Press: The MIT Press Cambridge, MA) · Zbl 0662.68029 |
| [22] | Sato, M.; Kameyama, Y., Constructive programming in SST, (Proc. Japanese—Czechoslovak Seminar on Theoretical Foundations of Knowledge Information Processing (1990), INORGA) |
| [23] | Takayama, Y., QPC: QJ-based proof compiler — simple examples and analysis, (Proc. European Symp. on Programming ’88. Proc. European Symp. on Programming ’88, Lecture Notres in Computer Science, Vol. 300 (1988), Springer: Springer Berlin) |
| [24] | Takayama, Y., \(QPC_2\): A constructive calculus with parameterized specifications, J. Symbolic Comput. (1993), to appear · Zbl 0804.68085 |
| [25] | Takayama, Y., Extraction of redundancy-free programs from constructive natural deduction proofs, J. Symbolic Comput., 12, 1 (1991) · Zbl 0731.68079 |
| [26] | Tatsuta, M., Realizability interpretation of coinductive definitions and program synthesis with streams, (Proc. Internat. Conf. on Fifth Generation Computer Systems 1992, Vol. 2 (1992), Institute for New Generation Computer Technology, OHMSHA) · Zbl 0860.03028 |
| [27] | (Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344 (1973), Springer: Springer Berlin) · Zbl 0275.02025 |
| [28] | Troelstra, A. S., Choice sequences, (Intuitionistic Mathematics (1977), Clarendon: Clarendon Oxford) · Zbl 0323.02040 |
| [29] | Troelstra, A. S.; van Dalen, D., Constructivism in Mathematics, An Introduction, (Studies in Logic and the Foundation of Mathematics, Vol 121 (1988), North-Holland: North-Holland Amsterdam). (Studies in Logic and the Foundation of Mathematics, Vol 123 (1988), North-Holland: North-Holland Amsterdam) · Zbl 0653.03040 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
