{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:53:53Z","timestamp":1725519233438},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540890195"},{"type":"electronic","value":"9783540890201"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-89020-1_14","type":"book-chapter","created":{"date-parts":[[2008,10,14]],"date-time":"2008-10-14T09:44:44Z","timestamp":1223977484000},"page":"184-200","source":"Crossref","is-referenced-by-count":0,"title":["A Single-Step Term-Graph Reduction System for Proof Assistants"],"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":"14_CR1","unstructured":"van Eekelen, M., Plasmeijer, R.: Concurrent CLEAN language report (version 1.3). Technical Report CSI\u2013R9816, Radboud University Nijmegen (1998)"},{"issue":"5","key":"14_CR2","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":"14_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods: Applications and Technology","year":"2007","unstructured":"Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.): FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346. Springer, Heidelberg (2007)"},{"key":"14_CR4","unstructured":"Moran, A.: Report on the First Commercial Users of Functional Programming Workshop. SIGPLAN Notices\u00a039(12) (2004)"},{"key":"14_CR5","series-title":"LNCS Tutorial Series","volume-title":"2nd Central-European Functional Programming School, CEFP 2007","author":"M. Mol de","year":"2008","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: Proving properties of lazy functional programs with SPARKLE. In: Horv\u00e1th, Z. (ed.) 2nd Central-European Functional Programming School, CEFP 2007, Cluj-Napoca, Romania. LNCS Tutorial Series. Springer, Heidelberg (to appear, 2008)"},{"key":"14_CR6","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. de Mol","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":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11431664_11","volume-title":"Implementation and Application of Functional Languages","author":"M. Dowse","year":"2005","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.J., Trinder, P. (eds.) IFL 2004. LNCS, vol.\u00a03474, pp. 177\u2013194. Springer, Heidelberg (2005)"},{"key":"14_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 I\/O - a paradigm comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol.\u00a02312, pp. 72\u201388. Springer, Heidelberg (2002)"},{"key":"14_CR9","unstructured":"Tejfel, M., Horv\u00e1th, Z., Kozsik, T.: Extending the sparkle core language with object abstraction. Acta Cybern.\u00a017(2) (2006)"},{"key":"14_CR10","unstructured":"Horv\u00e1th, Z., Kozsik, T., Tejfel, M.: Proving invariants of functional programs. In: Kilpel\u00e4inen, P., P\u00e4ivinen, N. (eds.) SPLST, University of Kuopio, Department of Computer Science, pp. 115\u2013126 (2003)"},{"key":"14_CR11","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 5th Int. Symposium on Trends in Functional Programming, TFP 2004, M\u00fcnchen, Germany, Intellect, pp. 1\u201316 (2004)","DOI":"10.2307\/j.ctv36xw0k5.4"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Launchbury, J.: A natural semantics for lazy evaluation. In: Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, pp. 144\u2013154 (1993)","DOI":"10.1145\/158511.158618"},{"key":"14_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 (2007)"},{"key":"14_CR14","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: Proving confluence of term-graph reduction for sparkle. Technical Report ICIS\u2013R07012, Radboud University Nijmegen (2007)"},{"key":"14_CR15","doi-asserted-by":"publisher","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":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48515-5_4","volume-title":"Implementation of Functional Languages","author":"J.G. Hall","year":"1999","unstructured":"Hall, J.G., Baker-Finch, C.A., Trinder, P.W., King, D.J.: Towards an operational semantics for a parallel non-strict functional language. In: Hammond, K., Davie, T., Clack, C. (eds.) IFL 1998. LNCS, vol.\u00a01595, pp. 54\u201371. Springer, Heidelberg (1999)"},{"key":"14_CR17","first-page":"233","volume-title":"POPL 1995: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"Z.M. Ariola","year":"1995","unstructured":"Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: A call-by-need lambda calculus. In: POPL 1995: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 233\u2013246. ACM Press, New York (1995)"},{"issue":"3","key":"14_CR18","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1017\/S0960129507006093","volume":"17","author":"P. Baldan","year":"2007","unstructured":"Baldan, P., Bertolissi, C., Cirstea, H., Kirchner, C.: A rewriting calculus for cyclic higher-order term graphs. Mathematical Structures in Computer Science\u00a017(3), 363\u2013406 (2007)","journal-title":"Mathematical Structures in Computer Science"},{"volume-title":"Term graph rewriting: theory and practice","year":"1993","key":"14_CR19","unstructured":"Sleep, M.R., Plasmeijer, M.J., van Eekelen, M.C.J.D. (eds.): Term graph rewriting: theory and practice. John Wiley and Sons Ltd., Chichester (1993)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"issue":"3","key":"14_CR21","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1017\/S0960129507006111","volume":"17","author":"C. Grabmayer","year":"2007","unstructured":"Grabmayer, C.: A duality between proof systems for cyclic term graphs. Mathematical Structures in Computer Science\u00a017(3), 439\u2013484 (2007)","journal-title":"Mathematical Structures in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Applications of Graph Transformations with Industrial Relevance"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89020-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T07:56:23Z","timestamp":1684569383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89020-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540890195","9783540890201"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89020-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}