{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:55:44Z","timestamp":1725519344565},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540880585"},{"type":"electronic","value":"9783540880592"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88059-2_2","type":"book-chapter","created":{"date-parts":[[2008,9,26]],"date-time":"2008-09-26T03:03:29Z","timestamp":1222398209000},"page":"41-86","source":"Crossref","is-referenced-by-count":2,"title":["Proving Properties of Lazy Functional Programs with Sparkle"],"prefix":"10.1007","author":[{"given":"Maarten","family":"de Mol","sequence":"first","affiliation":[]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[]},{"given":"Rinus","family":"Plasmeijer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/1088348.1088355","volume-title":"Proceedings of the ACM SIGPLAN 2005 Haskell Workshop","author":"A. Abel","year":"2005","unstructured":"Abel, A., Benke, M., Bove, A., Hughes, J., Norell, U.: Verifying Haskell programs using constructive type theory. In: Leijen, D. (ed.) Proceedings of the ACM SIGPLAN 2005 Haskell Workshop, Tallinn, Estonia, pp. 62\u201374. ACM Press, New York (2005)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-17945-3_8","volume-title":"PARLE Parallel Architectures and Languages Europe","author":"H.P. Barendregt","year":"1987","unstructured":"Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol.\u00a0259, pp. 141\u2013158. Springer, Heidelberg (1987)"},{"key":"2_CR3","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1142\/9789812815149_0002","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation","author":"E. Barendsen","year":"1999","unstructured":"Barendsen, E., Smetsers, S.: Graph rewriting aspects of functional programming. In: Handbook of Graph Grammars and Computing by Graph Transformation, pp. 63\u2013102. World Scientific, Singapore (1999)"},{"key":"2_CR4","volume-title":"Introduction to Functional Programming using Haskell","author":"R.S. Bird","year":"1998","unstructured":"Bird, R.S.: Introduction to Functional Programming using Haskell, 2nd edn. Prentice-Hall, Englewood Cliffs (1998)","edition":"2"},{"key":"2_CR5","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-18317-5_20","volume-title":"Proceedings of the Functional Programming Languages and Computer Architecture","author":"T.H. Brus","year":"1987","unstructured":"Brus, T.H., van Eekelen, M.C.J.D., van Leer, M.O., Plasmeijer, M.J.: Clean: A language for functional graph writing. In: Proceedings of the Functional Programming Languages and Computer Architecture, pp. 364\u2013384. Springer, Heidelberg (1987)"},{"key":"2_CR6","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1007\/3-540-18317-5_24","volume-title":"Proc. of a conference on Functional programming languages and computer architecture","author":"G.L. Burn","year":"1987","unstructured":"Burn, G.L.: Evaluation transformers a model for the parallel evolution of functional languages. In: Proc. of a conference on Functional programming languages and computer architecture, pp. 446\u2013470. Springer, Heidelberg (1987)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-46028-4_5","volume-title":"Implementation of Functional Languages","author":"A. Butterfield","year":"2002","unstructured":"Butterfield, A., Strong, G.: Proving Correctness of Programs with I\/O - a paradigm comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol.\u00a02312, pp. 72\u201388. Springer, Heidelberg (2002)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-46028-4_5","volume-title":"Implementation of Functional Languages","author":"A. Butterfield","year":"2002","unstructured":"Butterfield, A., Strong, G.: Proving correctness of programs with io - a paradigm comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol.\u00a02312, pp. 72\u201387. Springer, Heidelberg (2002)"},{"key":"2_CR9","unstructured":"Coquand, T., Dybjer, P., Hughes, J., Sheeran, M.: Combining verification methods in software development. Project proposal, Chalmers Institute of Techology, Sweden (December 2001)"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1145\/1111320.1111056","volume":"41","author":"N.A. Danielsson","year":"2006","unstructured":"Danielsson, N.A., Hughes, J., Jansson, P., Gibbons, J.: Fast and loose reasoning is morally correct. SIGPLAN Not.\u00a041(1), 206\u2013217 (2006)","journal-title":"SIGPLAN Not."},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-46028-4_4","volume-title":"Implementation of Functional Languages","author":"M. Mol de","year":"2002","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem proving for functional programmers - Sparkle: A functional theorem prover. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol.\u00a02312, pp. 55\u201372. Springer, Heidelberg (2002)"},{"key":"2_CR12","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: A single-step term-graph reduction system for proof assistants. In: Sch\u00fcrr, A., Nagl, M., Z\u00fcndorf, A. (eds.) Proceedings of Selected and Invited Papers of Applications of Graph Transformations with Industrial Relevance, Third International Symposium, AGTIVE 2007, Kassel, Germany, pp. 181\u2013197 (2007)"},{"key":"2_CR13","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: The Mathematical Foundation of the Proof Assistant Sparkle. Technical Report ICIS\u2013R07025, Radboud University Nijmegen (November 2007)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","first-page":"177","volume-title":"IFL","author":"M. Dowse","year":"2004","unstructured":"Dowse, M., Butterfield, A., van Eekelen, M.C.J.D.: Reasoning About Deterministic Concurrent Functional I\/O. In: Grelck, C., Huch, F., Michaelson, G., Trinder, P.W. (eds.) IFL 2004. LNCS, vol.\u00a03474, pp. 177\u2013194. Springer, Heidelberg (2004)"},{"key":"2_CR15","first-page":"4","volume-title":"Functional Programming","author":"A. Gill","year":"1995","unstructured":"Gill, A.: The technology behind a graphical user interface for an equational reasoning assistant. In: Turner, D.N. (ed.) Functional Programming. Workshops in Computing, p. 4. Springer, Heidelberg (1995)"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1159842.1159856","volume-title":"Haskell 2006: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell","author":"A. Gill","year":"2006","unstructured":"Gill, A.: Introducing the haskell equational reasoning assistant. In: Haskell 2006: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, pp. 108\u2013109. ACM Press, New York (2006)"},{"key":"2_CR17","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the Eleventh Conference on the Mathematical Foundations of Programming Semantics","author":"A. Gordon","year":"1995","unstructured":"Gordon, A.: Bisimilarity as a theory of functional programming. In: Proceedings of the Eleventh Conference on the Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol.\u00a01. Elsevier Science B.V, Amsterdam (1995)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: a mechanised logic of computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Berlin (1979)"},{"key":"2_CR19","unstructured":"Horv\u00e1th, Z., Kozsik, T., Tejfel, M.: Proving invariants of functional programs. In: Kilpel\u00e4inen, P., P\u00e4ivinen, N. (eds.) SPLST. Department of Computer Science, pp. 115\u2013126. University of Kuopio (2003)"},{"issue":"5","key":"2_CR20","first-page":"1","volume":"27","author":"P. Hudak","year":"1992","unstructured":"Hudak, P., Jones, S.L.P., Wadler, P., Boutel, B., Fairbairn, J., Fasel, J.H., Guzm\u00e1n, M.M., Hammond, K., Hughes, J., Johnsson, T., Kieburtz, R.B., Nikhil, R.S., Partain, W., Peterson, J.: Report on the Programming Language Haskell, A Non-strict, Purely Functional Language. SIGPLAN Notices\u00a027(5), R1\u2013R164 (1992)","journal-title":"SIGPLAN Notices"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"van Kesteren, R., van Eekelen, M., de Mol, M.: Proof support for general type classes. In: Loidl, H.-W. (ed.) Trends in Functional Programming 5: Selected papers from the Fifth International Symposium on Trends in Functional Programming, TFP 2004, M\u00fcnchen, Germany, Intellect, pp. 1\u201316 (2004)","DOI":"10.2307\/j.ctv36xw0k5.4"},{"key":"2_CR22","first-page":"151","volume-title":"Proceedings of the Glasgow Functional Progamming Workshop","author":"S. Mintchev","year":"1994","unstructured":"Mintchev, S.: Mechanized reasoning about functional programs. In: Hammond, K., Turner, D., Sansom, P. (eds.) Proceedings of the Glasgow Functional Progamming Workshop, pp. 151\u2013167. Springer, Heidelberg (1994)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"582","DOI":"10.1007\/3-540-45319-9_41","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001)","author":"T. Noll","year":"2001","unstructured":"Noll, T., Fredlund, L., Gurov, D.: The evt erlang verification tool. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 582\u2013585. Springer, Heidelberg (2001)"},{"key":"2_CR24","unstructured":"Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS Language Reference (version 2.4) (2001), http:\/\/pvs.csl.sri.com\/doc\/pvs-prover-guide.pdf"},{"key":"2_CR25","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and Computation","author":"L.C. Paulson","year":"1987","unstructured":"Paulson, L.C.: Logic and Computation. Cambridge University Press, Cambridge (1987)"},{"key":"2_CR26","unstructured":"Paulson, L.C.: The Isabelle Reference Manual. University of Cambridge (2007), http:\/\/isabelle.in.tum.de\/doc\/ref.pdf"},{"key":"2_CR27","volume-title":"Functional Programming and Parallel Graph Rewriting","author":"R. Plasmeijer","year":"1993","unstructured":"Plasmeijer, R., van Eekelen, M.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley Publishing Company, Reading (1993)"},{"issue":"6","key":"2_CR28","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/606666.606670","volume":"34","author":"R. Plasmeijer","year":"1999","unstructured":"Plasmeijer, R., van Eekelen, M.: Keep it clean: a unique approach to functional programming. SIGPLAN Not.\u00a034(6), 23\u201331 (1999)","journal-title":"SIGPLAN Not."},{"key":"2_CR29","unstructured":"Plasmeijer, R., van Eekelen, M.: Concurrent CLEAN Language Report (version 2.0) (December 2001), http:\/\/www.cs.ru.nl\/~clean\/"},{"key":"2_CR30","unstructured":"Tejfel, M., Horv\u00e1th, Z., Kozsik, T.: Extending the sparkle core language with object abstraction. Acta Cybern.\u00a017(2) (2006)"},{"key":"2_CR31","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual (version 7.3). Inria (2002), http:\/\/pauillac.inria.fr\/cdrom\/www\/coq\/doc\/main.html"},{"issue":"1","key":"2_CR32","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1017\/S0956796897002967","volume":"8","author":"P.W. Trinder","year":"1998","unstructured":"Trinder, P.W., Hammond, K., Loidl, H.-W., Jones, S.L.P.: Algorithm + strategy = parallelism. J. Funct. Program.\u00a08(1), 23\u201360 (1998)","journal-title":"J. Funct. Program."},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11964681_3","volume-title":"Implementation and Application of Functional Languages","author":"M. Eekelen van","year":"2006","unstructured":"van Eekelen, M., de Mol, M.: Proof tool support for explicit strictness. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol.\u00a04015, pp. 37\u201354. Springer, Heidelberg (2006)"},{"key":"2_CR34","unstructured":"Winstanley, N.: Era User Manual, version 2.0. University of Glasgow (March 1998), http:\/\/www.dcs.gla.ac.uk\/~nww\/Era\/Era.html"}],"container-title":["Lecture Notes in Computer Science","Central European Functional Programming School"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88059-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T02:34:08Z","timestamp":1684550048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88059-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540880585","9783540880592"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88059-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}