{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T15:28:54Z","timestamp":1765294134407},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540115762"},{"type":"electronic","value":"9783540393085"}],"license":[{"start":{"date-parts":[[1982,1,1]],"date-time":"1982-01-01T00:00:00Z","timestamp":378691200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1982]]},"DOI":"10.1007\/bfb0012782","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T13:00:52Z","timestamp":1132750852000},"page":"348-359","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":63,"title":["Results on the propositional \u03bc-calculus"],"prefix":"10.1007","author":[{"given":"Dexter","family":"Kozen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,10,22]]},"reference":[{"key":"31_CR1","unstructured":"P. Hitchcock and D.M.R. Park, Induction Rules and Termination Proofs, Proc. 1st ICALP, 1973, 225\u2013251."},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0304-3975(81)90019-0","volume":"14","author":"D. Kozen","year":"1981","unstructured":"D. Kozen and R. Parikh, An Elementary Proof of the Completeness of PDL, TCS 14 (1981), 113\u2013118.","journal-title":"TCS"},{"key":"31_CR3","first-page":"352","volume":"85","author":"D. Kozen","year":"1980","unstructured":"D. Kozen, A Representation Theorem for Models of *-free PDL, Proc. 7th ICALP, Springer LNCS 85 (1980), 352\u2013362.","journal-title":"Springer LNCS"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"D. Kozen, On the Duality of Dynamic Algebras and Kripke Models, Proc. Workshop on Logic of, Programs, Springer LNCS 125, 1\u201311.","DOI":"10.1007\/3-540-11160-3_1"},{"key":"31_CR5","first-page":"167","volume":"131","author":"D. Kozen","year":"1982","unstructured":"D. Kozen, On Induction vs. *-continuity, Proc. Workshop on Logics of Programs, Springer LNCS 131 (1982), 167\u2013176.","journal-title":"Springer LNCS"},{"key":"31_CR6","unstructured":"D.M.R. Park, Fixpoint Induction and proof of program semantics, Mach. Int. 5, ed. Meltzer and Michie, Edinburgh Univ. Press, 1970, 59\u201378."},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"V.R. Pratt, A Decidable \u039c-calculus (Preliminary Report), Proc. 22nd FOCS, Oct. 1981, 421\u2013427.","DOI":"10.1109\/SFCS.1981.4"},{"key":"31_CR8","first-page":"231","volume":"20","author":"V.R. Pratt","year":"1980","unstructured":"V.R. Pratt, A near optimal method for reasoning about action, JCSS 20 (1980), 231\u2013254.","journal-title":"JCSS"},{"key":"31_CR9","volume-title":"A Theory of Programs","author":"D. Scott","year":"1969","unstructured":"D. Scott and J. deBakker, A Theory of Programs, unpublished, IBM, Vienna, 1969."},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"R. Streett, Propositional Dynamic Logic of Looping and Converse, Proc. 13th STOC, May 1981, 375\u2013383.","DOI":"10.1145\/800076.802492"},{"issue":"1","key":"31_CR11","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"Ashok K. Chandra","year":"1981","unstructured":"A. Chandra, D. Kozen, L. Stockmeyer, Alternation, JACM, Jan. 1981.","journal-title":"Journal of the ACM"},{"key":"31_CR12","unstructured":"J. deBakker, Mathematical Theory of Program Correctness, Prentice-Hall, 1980."},{"key":"31_CR13","unstructured":"J. deBakker and W. deRoever, A Calculus for Recursive Program Schemes, Proc. 1st ICALP, 1973, 167\u2013196."},{"key":"31_CR14","volume-title":"Ph.D. Thesis","author":"W.P. deRoever","year":"1974","unstructured":"W.P. deRoever, Recursive. Program Schemes: Semantics and Proof Theory, Ph.D. Thesis, Free University, Amsterdam, 1974."},{"key":"31_CR15","first-page":"52","volume":"131","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke, Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic, Proc. Workshop on Logics of Programs, Springer LNCS 131 (1982), 52\u201371.","journal-title":"Springer LNCS"},{"issue":"2","key":"31_CR16","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"Michael J. Fischer","year":"1979","unstructured":"M. Fischer and R. Ladner, Propositional Dynamic Logic of Regular Programs, JCSS 18:2 (79).","journal-title":"Journal of Computer and System Sciences"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"J. Halpern and J. Reif, The Propositional Dynamic Logic of Deterministic, Well-Structured Programs, (extended abstract), Proc. 22nd FOCS, Oct. 1981, 322\u2013334.","DOI":"10.1109\/SFCS.1981.49"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012782","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:57:26Z","timestamp":1558270646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012782"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982]]},"ISBN":["9783540115762","9783540393085"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0012782","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1982]]},"assertion":[{"value":"22 October 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}