{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:22:26Z","timestamp":1754482946125},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633792"},{"type":"electronic","value":"9783540695264"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0028388","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T01:50:11Z","timestamp":1132624211000},"page":"89-104","source":"Crossref","is-referenced-by-count":7,"title":["Possibly infinite sequences in theorem provers: A comparative study"],"prefix":"10.1007","author":[{"given":"Marco","family":"Devillers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Griffioen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olaf","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"7_CR1","series-title":"PhD thesis","volume-title":"A HOL Basis for Reasoning about Functional Programs","author":"S. Agerholm","year":"1994","unstructured":"Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. PhD thesis, University of Aarhus, Denmark, 1994."},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. J. Symbolic Logic, 5:56\u201368, 1940.","journal-title":"J. Symbolic Logic"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Ching-Tsun Chou and Doron Peled. Formal verification of a partial-order reduction technique for model checking. In T. Margaria and B. Steffen, editors, Proc. 2nd Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61042-1_48"},{"key":"7_CR4","unstructured":"Marco Devillers and David Griffioen. A formalization of finite and infinite sequences in PVS. Technical Report CSI-89702, Computing Science Institute, University of Nijmegen, 1997."},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(96)88189-9","volume":"81","author":"S. Feferman","year":"1996","unstructured":"Solomom Feferman. Computation on abstract data types. the extensional approach, with an application to streams. Annals of Pure and Applied Logic, 81:75\u2013113, 1996.","journal-title":"Annals of Pure and Applied Logic"},{"key":"7_CR6","unstructured":"M.C.J. Gordon and T.F. Melham. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"U. Hensel and B. Jacobs. Proof principles for datatypes with iterated recursion. Technical Report CSI-89703, Computing Science Institute, University of Nijmegen, 1997.","DOI":"10.1007\/BFb0026991"},{"issue":"3","key":"7_CR8","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Leslie Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Francois Leclerc and Christine Paulin-Mohring. Programming with streams in Coq, a case study: the sieve of eratosthenes. In H. Barendregt and T. Nipkow, editors, Proc. Types for Proofs and Programs (TYPES'93), volume 806 of Lecture Notes in Computer Science, 1993.","DOI":"10.1007\/3-540-58085-9_77"},{"issue":"3","key":"7_CR10","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Nancy Lynch and Mark Tuttle. An introduction to Input\/Output automata. CWI Quarterly, 2(3):219\u2013246, 1989.","journal-title":"CWI Quarterly"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Olaf M\u00fcller and Tobias Nipkow. Traces of I\/O-Automata in Isabelle\/HOLCF. In Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'97), Lecture Notes in Computer Science. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0030627"},{"key":"7_CR12","unstructured":"Olaf M\u00fcller and Konrad Slind. Isabelle\/HOL as a platform for partiality. In CADE-13 Workshop: Mechanization of Partial Functions, New Brunswick, pages 85\u201396, 1996."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and Konrad Slind. 1\/O automata in Isabelle\/HOL. In P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 101\u2013119. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60579-7_6"},{"issue":"2","key":"7_CR14","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Logic and Computation. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. J. Automated Reasoning, 7, 1997.","DOI":"10.1093\/logcom\/7.2.175"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Franz Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E.T. Schubert, P.J. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 293\u2013307. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_72"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028388","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T22:48:49Z","timestamp":1586558929000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028388"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633792","9783540695264"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0028388","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}