{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:01:30Z","timestamp":1767927690660,"version":"3.49.0"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,10,30]],"date-time":"2008-10-30T00:00:00Z","timestamp":1225324800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s10990-008-9038-0","type":"journal-article","created":{"date-parts":[[2008,10,29]],"date-time":"2008-10-29T20:30:55Z","timestamp":1225312255000},"page":"377-409","source":"Crossref","is-referenced-by-count":13,"title":["Adapting functional programs to higher order logic"],"prefix":"10.1007","volume":"21","author":[{"given":"Scott","family":"Owens","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,10,30]]},"reference":[{"issue":"1","key":"9038_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796801004191","volume":"12","author":"A. Abel","year":"2002","unstructured":"Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. J. Funct. Program. 12(1), 1\u201341 (2002)","journal-title":"J. Funct. Program."},{"key":"9038_CR2","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne\u2014a language with dependent types. In: International Conference on Functional Programming, pp. 239\u2013250 (1998)","DOI":"10.1145\/291251.289451"},{"key":"9038_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs (TYPES 2000)","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Types for Proofs and Programs (TYPES 2000). Lecture Notes in Computer Science, vol. 2277, pp. 24\u201340. Springer, New York (2002)"},{"key":"9038_CR4","volume-title":"Second IEEE International Conference on Software Engineering and Formal Methods (SEFM 2004)","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Second IEEE International Conference on Software Engineering and Formal Methods (SEFM 2004). IEEE Computer Society Press, Silver Spring (2004)"},{"issue":"1","key":"9038_CR5","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(86)90088-5","volume":"48","author":"G. Berry","year":"1986","unstructured":"Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theor. Comput. Sci. 48(1), 117\u2013126 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"9038_CR6","series-title":"Texts in Theoretical Computer Science, An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, An EATCS Series. Springer, New York (2004)"},{"key":"9038_CR7","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, New York (1979)"},{"issue":"4","key":"9038_CR8","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"J. Brzozowski","year":"1964","unstructured":"Brzozowski, J.: Derivatives of Regular Expressions. J. ACM 11(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"issue":"2","key":"9038_CR9","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9038_CR10","unstructured":"Cockett, R., Fukushima, T.: About charity. Technical Report TR 92\/480\/18, Department of Computer Science, University of Calgary (1992)"},{"key":"9038_CR11","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/91556.91622","volume-title":"Proceedings of the 1990 ACM Conference on LISP and Functional Programming, Nice","author":"O. Danvy","year":"1990","unstructured":"Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, Nice, New York, NY, pp. 151\u2013160. ACM, New York (1990)"},{"key":"9038_CR12","doi-asserted-by":"crossref","unstructured":"Danvy, O., Nielsen, L.R.: Defunctionalization at work. Technical Report RS-01-23, BRICS (2001). Extended version of an article appearing in 3rd International Conference on Principles and Practice of Declarative Programming, PPDP\u201901 Proceedings, pp. 162\u2013174 (2001)","DOI":"10.1145\/773184.773202"},{"key":"9038_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Proceedings of TPHOLs 2003","author":"P. Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) Proceedings of TPHOLs 2003. Lecture Notes in Computer Science, vol. 2758, pp. 188\u2013203. Springer, New York (2003)"},{"key":"9038_CR14","doi-asserted-by":"crossref","unstructured":"Farmer, W., Guttman, J., Thayer, J.: IMPS: an interactive mathematical proof system. In: Stickel, M. (ed.) Tenth International Conference on Automated Deduction (CADE). Kaiserslautern, pp. 653\u2013654 (1990)","DOI":"10.1007\/3-540-52885-7_126"},{"issue":"4","key":"9038_CR15","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.-C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.-C.: Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13(4), 709\u2013745 (2003)","journal-title":"J. Funct. Program."},{"key":"9038_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1007\/978-3-540-27836-8_53","volume-title":"ICALP 2004","author":"A. Frisch","year":"2004","unstructured":"Frisch, A., Cardelli, L.: Greedy regular expression matching. In: ICALP 2004. Lecture Notes in Computer Science, vol. 3142, pp. 618\u2013629. Springer, New York (2004)"},{"key":"9038_CR17","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/289423.289455","volume-title":"Proceedings of the third ACM SIGPLAN International Conference on Functional Programming","author":"J. Gibbons","year":"1998","unstructured":"Gibbons, J., Jones, G.: The under-appreciated unfold. In: Proceedings of the third ACM SIGPLAN International Conference on Functional Programming, pp. 273\u2013279. ACM Press, Baltimore (1998)"},{"key":"9038_CR18","first-page":"154","volume-title":"Proceedings of the Second International Symposium on Static Analysis","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Termination analysis for functional programs using term orderings. In: Proceedings of the Second International Symposium on Static Analysis, pp. 154\u2013171. Springer, New York (1995)"},{"issue":"1","key":"9038_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"J. Giesl","year":"1997","unstructured":"Giesl, J.: Termination of nested and mutually recursive algorithms. J. Autom. Reason. 19(1), 1\u201329 (1997)","journal-title":"J. Autom. Reason."},{"key":"9038_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0097782","volume-title":"Proceedings of ICALP\u201998","author":"E. Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural recursive definitions in type theory. In: Proceedings of ICALP\u201998. Lecture Notes in Computer Science, vol. 1443. Springer, New York (1998)"},{"key":"9038_CR21","volume-title":"Introduction to HOL, a Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"9038_CR22","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: A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol.\u00a078. Springer, New York (1979)"},{"key":"9038_CR23","doi-asserted-by":"crossref","unstructured":"Gordon, M., Iyoda, J., Owens, S., Slind, K.: Automatic formal synthesis of hardware from higher order logic. In: Proceedings of Fifth International Workshop on Automated Verification of Critical Systems (AVoCS). ENTCS, vol. 145 (2005)","DOI":"10.1016\/j.entcs.2005.10.003"},{"key":"9038_CR24","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-1-4757-3188-0_8","volume-title":"Computer-Aided Reasoning Case Studies","author":"D. Greve","year":"2000","unstructured":"Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Kaufmann, M., Manolios, P., Moore, J. (eds.) Computer-Aided Reasoning Case Studies, pp. 113\u2013135. Kluwer Academic, Dordrecht (2000)"},{"issue":"1","key":"9038_CR25","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1017\/S0956796807006338","volume":"18","author":"D.A. Greve","year":"2008","unstructured":"Greve, D.A., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz-Reina, J.L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1), 15\u201346 (2008)","journal-title":"J. Funct. Program."},{"key":"9038_CR26","unstructured":"Hagino, T.: A categorical programming language. Ph.D. thesis, University of Edinburgh (1987). Also published as ECS-LFCS-87-38"},{"issue":"4","key":"9038_CR27","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1017\/S0956796899003378","volume":"9","author":"R. Harper","year":"1999","unstructured":"Harper, R.: Proof-directed debugging. J. Funct. Program. 9(4), 463\u2013470 (1999)","journal-title":"J. Funct. Program."},{"key":"9038_CR28","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-60275-5_66","volume-title":"Proceedings of the 1995 International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Inductive definitions: automation and application. In: Schubert, E.T., Windley, P.J., Alves-Fos, J. (eds.) Proceedings of the 1995 International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, pp. 200\u2013213. Springer, New York (1995)"},{"issue":"6","key":"9038_CR29","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1017\/S0956796802004410","volume":"13","author":"H. Hosoya","year":"2003","unstructured":"Hosoya, H., Pierce, B.: Regular expression pattern matching for XML. J. Funct. Program. 13(6), 961\u20131004 (2003)","journal-title":"J. Funct. Program."},{"key":"9038_CR30","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Inf. 11, 31\u201355 (1978)","journal-title":"Acta Inf."},{"key":"9038_CR31","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic, Dordrecht (2000)"},{"key":"9038_CR32","volume-title":"Computer-Aided Reasoning: Case Studies","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: Case Studies. Kluwer Academic, Dordrecht (2000)"},{"issue":"1","key":"9038_CR33","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1017\/S0956796803004854","volume":"14","author":"C. Kreitz","year":"2004","unstructured":"Kreitz, C.: Building reliable, high-performance networks with the nuprl proof development system. J.\u00a0Funct. Program. 14(1), 21\u201368 (2004)","journal-title":"J.\u00a0Funct. Program."},{"key":"9038_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking and Abstract Interpretation: Third International Workshop (VMCAI 2002)","author":"S. Krsti\u0107","year":"2002","unstructured":"Krsti\u0107, S., Matthews, J.: Verifying BDD algorithms through monadic interpretation. In: Cortesi, A. (ed.) Verification, Model Checking and Abstract Interpretation: Third International Workshop (VMCAI 2002). Lecture Notes in Computer Science, vol. 2294. Springer, New York (2002)"},{"key":"9038_CR35","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"9038_CR36","volume-title":"ACM Symposium on Principles of Programming Languages","author":"J.R. Lewis","year":"2000","unstructured":"Lewis, J.R., Shields, M.B., Meijer, E., Launchbury, J.: Implicit parameters: dynamic scoping with static types. In: Reps, T. (ed.) ACM Symposium on Principles of Programming Languages, Boston, Massachusetss, USA. ACM Press, New York (2000)"},{"key":"9038_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"ESOP 2007","author":"G. Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: ESOP 2007. Lecture Notes in Computer Science, vol. 4421. Springer, New York (2007)"},{"key":"9038_CR38","volume-title":"Proceedings of the 17th ACM Symposium on Operating System Principles","author":"X. Liu","year":"1999","unstructured":"Liu, X., Kreitz, C., Renesse, R., Hickey, J., Hayden, M., Birman, K., Constable, R.: Building reliable, high-performance communication systems from components. In: Proceedings of the 17th ACM Symposium on Operating System Principles. ACM Press, New York (1999)"},{"key":"9038_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification (CAV)","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4144, pp. 401\u2013414. Springer, New York (2006)"},{"key":"9038_CR40","unstructured":"March\u00e9, C.: A simple library for regular expressions. Regexp library for OCaml, available at http:\/\/www.lri.fr\/~marche\/regexp\/ (2002)"},{"key":"9038_CR41","volume-title":"Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics","author":"J. Matthews","year":"1999","unstructured":"Matthews, J.: Recursive definition over coinductive types. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Thery, L. (eds.) Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201999, Nice. Springer, New York (1999)"},{"issue":"5","key":"9038_CR42","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1017\/S0956796803004982","volume":"14","author":"D. McIlroy","year":"2004","unstructured":"McIlroy, D.: Enumerating the strings of regular languages (Functional Pearl). J. Funct. Program. 14(5), 503\u2013518 (2004)","journal-title":"J. Funct. Program."},{"issue":"2","key":"9038_CR43","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"J. Moore","year":"2003","unstructured":"Moore, J., Manolios, P.: Partial functions in ACL2. J. Autom. Reason. 31(2), 107\u2013127 (2003)","journal-title":"J. Autom. Reason."},{"key":"9038_CR44","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., Oheimb, D.v, Slotosch, O.: HOLCF=HOL+LCF. J. Funct. Program. 9, 191\u2013223 (1999)","journal-title":"J. Funct. Program."},{"key":"9038_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0052355","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1479, pp. 1\u201315. Springer, New York (1998). Invited talk"},{"key":"9038_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol.\u00a02283. Springer, New York (2002)"},{"key":"9038_CR47","unstructured":"Nishihara, T., Minamide, Y.: Depth first search. Entry in the Isabelle Archive of Formal Proofs (2004)"},{"key":"9038_CR48","unstructured":"Norrish, M., Slind, K.: HOL-4 manuals. Available at http:\/\/hol.sourceforge.net\/ (1998\u20132005)"},{"key":"9038_CR49","unstructured":"Owens, S., Flatt, M., Shivers, O., McMullan, B.: Parsing tools in scheme. In: Proceedings of the 2004 Scheme Workshop (2004)"},{"key":"9038_CR50","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide. SRI Computer Science Laboratory. Available at http:\/\/pvs.csl.sri.com\/documentation.shtml (2001)"},{"issue":"3","key":"9038_CR51","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Rudnicki, P., Trybulec, A.: On equivalents of well-foundedness. J. Autom. Reason. 23(3), 197\u2013234 (1999)","journal-title":"J. Autom. Reason."},{"key":"9038_CR52","unstructured":"Shankar, N.: Steps towards mechanizing program transformations using PVS. In: Moeller, B. (ed.) Mathematics of Program Construction, Third International Conference (MPC\u201995), Kloster Irsee, Germany, pp. 50\u201366 (1995)"},{"key":"9038_CR53","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001","author":"N. Shankar","year":"2001","unstructured":"Shankar, N.: Static analysis for safe destructive updates in a functional language. In: Pettorossi, A. (ed.) Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001. Lecture Notes in Computer Science, vol. 2372, pp. 1\u201324. Springer, New York (2001)"},{"key":"9038_CR54","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BFb0028400","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1997","unstructured":"Slind, K.: Derivation and use of induction schemes in higher order logic. In: Theorem Proving in Higher Order Logics, Murrary Hill, New Jersey, USA, pp. 275\u2013291. Springer, New York (1997)"},{"key":"9038_CR55","unstructured":"Slind, K.: Reasoning about terminating functional programs. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen. Available at http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/1999\/slind.html (1999)"},{"key":"9038_CR56","doi-asserted-by":"crossref","unstructured":"Slind, K.: Wellfounded schematic definitions. In: McAllester, D. (ed.) Proceedings of the Seventeenth International Conference on Automated Deduction CADE-17, vol. 1831. Pittsburgh, Pennsylvania, pp.\u00a045\u201363. Springer, New York","DOI":"10.1007\/10721959_4"},{"key":"9038_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/10930755_7","volume-title":"Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rome, Italy, Proceedings","author":"K. Slind","year":"2003","unstructured":"Slind, K., Hurd, J.: Applications of polytypism in theorem proving. In: Basin, D., Wolff, B. (eds.) Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rome, Italy, Proceedings. Lecture Notes in Computer Science, vol. 2758, pp. 103\u2013119. Springer, New York (2003)"},{"issue":"6","key":"9038_CR58","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1145\/363347.363387","volume":"11","author":"K. Thompson","year":"1968","unstructured":"Thompson, K.: Programming techniques: regular expression search algorithm. Commun. ACM 11(6), 419\u2013422 (1968)","journal-title":"Commun. ACM"},{"key":"9038_CR59","unstructured":"Thompson, S.: Regular expressions and automata using Haskell. Technical Report 5-00, Computing Laboratory, University of Kent. Available at http:\/\/www.cs.ukc.ac.uk\/pubs\/2000\/958 (2000)"},{"key":"9038_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60675-0_35","volume-title":"Functional Programming Languages in Education","author":"D.A. Turner","year":"1995","unstructured":"Turner, D.A.: Elementary strong functional programming. In: Functional Programming Languages in Education. Lecture Notes in Computer Science, vol. 1022, pp. 1\u201313. Springer, New York (1995)"},{"key":"9038_CR61","unstructured":"van der Vlist, E.: Relax NG. O\u2019Reilly (2003)"},{"key":"9038_CR62","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H. Xi","year":"2002","unstructured":"Xi, H.: Dependent types for program termination verification. J. Higher-Order Symb. Comput. 15, 91\u2013131 (2002)","journal-title":"J. Higher-Order Symb. Comput."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-008-9038-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-008-9038-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-008-9038-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:29:41Z","timestamp":1559352581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-008-9038-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10,30]]},"references-count":62,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["9038"],"URL":"https:\/\/doi.org\/10.1007\/s10990-008-9038-0","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,10,30]]}}}