{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T01:40:21Z","timestamp":1743298821192,"version":"3.40.3"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,6,8]],"date-time":"2012-06-08T00:00:00Z","timestamp":1339113600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10817-012-9253-6","type":"journal-article","created":{"date-parts":[[2012,6,7]],"date-time":"2012-06-07T15:41:07Z","timestamp":1339083667000},"page":"383-421","source":"Crossref","is-referenced-by-count":1,"title":["A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions"],"prefix":"10.1007","volume":"50","author":[{"given":"David","family":"Sabel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,8]]},"reference":[{"key":"9253_CR1","unstructured":"ACL2 Website: http:\/\/www.cs.utexas.edu\/~moore\/acl2 (2011). Accessed 1 May 2012"},{"key":"9253_CR2","unstructured":"Agda Website: http:\/\/wiki.portal.chalmers.se\/agda (2011). Accessed 1 May 2012"},{"key":"9253_CR3","unstructured":"Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, New York (1984)"},{"key":"9253_CR4","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H Barringer","year":"1984","unstructured":"Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Inform. 21, 251\u2013269 (1984)","journal-title":"Acta Inform."},{"key":"9253_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9253_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In: Antoy, S., Albert, E. (eds.) Proc. PPDP \u201908, pp. 89\u201396. ACM, New York, NY, USA (2008)","DOI":"10.1145\/1389449.1389461"},{"key":"9253_CR7","unstructured":"Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers: an overview. Math. Struct. Comput. Sci. (2012, to appear). Preprint available at http:\/\/www4.informatik.tu-muenchen.de\/~krauss\/papers\/recursion.pdf dates from 2011"},{"issue":"1","key":"9253_CR8","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/321864.321875","volume":"22","author":"RS Boyer","year":"1975","unstructured":"Boyer, R.S., Moore, J.S.: Proving theorems about lisp functions. J. ACM 22(1), 129\u2013144 (1975)","journal-title":"J. ACM"},{"issue":"3","key":"9253_CR9","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1145\/828.1882","volume":"31","author":"RS Boyer","year":"1984","unstructured":"Boyer, R.S., Moore, J.S.: A mechanical proof of the unsolvability of the halting problem. J. ACM 31(3), 441\u2013458 (1984)","journal-title":"J. ACM"},{"key":"9253_CR10","unstructured":"Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Morgan, C., Woodcock, J.C.P. (eds.) 3rd Refinement Workshop, pp.\u00a051\u201369. Springer (1991)"},{"key":"9253_CR11","doi-asserted-by":"crossref","unstructured":"Chiba, Y., Aoto, T., Toyama, Y.: Program transformation by templates based on term rewriting. In: Barahona, P., Felty, A.P. (eds.) Proc. PPDP \u201905, pp. 59\u201369. ACM (2005)","DOI":"10.1145\/1069774.1069780"},{"key":"9253_CR12","unstructured":"Coq Website: http:\/\/coq.inria.fr\/ (2011). Accessed 1 May 2012"},{"issue":"2\/3","key":"9253_CR13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"issue":"3","key":"9253_CR14","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0168-0072(93)90144-3","volume":"64","author":"WM Farmer","year":"1993","unstructured":"Farmer, W.M.: A simple type theory with partial functions and subtypes. Ann. Pure Appl. Logic 64(3), 211\u2013240 (1993)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9253_CR15","unstructured":"Farmer, W.M.: Mechanizing the traditional approach to partial functions. In: Farmer, W., Kerber, M., Kohlhase, M. (eds.) Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 27\u201332. CADE-13, Rutgers University, New Brunswick, New Jersey. Available from http:\/\/imps.mcmaster.ca\/wmfarmer\/ (1996). Accessed 1 May 2012"},{"key":"9253_CR16","doi-asserted-by":"crossref","unstructured":"Farmer, W.M.: Formalizing undefinedness arising in calculus. In: Basin, D.A., Rusinowitch, M. (eds.) Proc. IJCAR \u201904. Lecture Notes in Comput. Sci., vol. 3097, pp. 475\u2013489. Springer (2004)","DOI":"10.1007\/978-3-540-25984-8_35"},{"issue":"2","key":"9253_CR17","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"WM Farmer","year":"1993","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213\u2013248 (1993)","journal-title":"J. Autom. Reason."},{"key":"9253_CR18","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103, 235\u2013271 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9253_CR19","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1023\/A:1005702928286","volume":"18","author":"S Finn","year":"1997","unstructured":"Finn, S., Fourman, M.P., Longley, J.: Partial functions in a total setting. J. Autom. Reason. 18(1), 85\u2013104 (1997)","journal-title":"J. Autom. Reason."},{"issue":"3\u20134","key":"9253_CR20","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1016\/j.ipl.2008.02.005","volume":"107","author":"J Fitzgerald","year":"2008","unstructured":"Fitzgerald, J., Jones, C.: The connection between two ways of reasoning about partial functions. Inf. Process. Lett. 107(3\u20134), 128\u2013132 (2008)","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"9253_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1006408829523","volume":"26","author":"J Giesl","year":"2001","unstructured":"Giesl, J.: Induction proofs with partial functions. J. Autom. Reason. 26(1), 1\u201349 (2001)","journal-title":"J. Autom. Reason."},{"key":"9253_CR22","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA (1993)"},{"issue":"4","key":"9253_CR23","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1093\/jigpal\/jzi032","volume":"13","author":"R H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Log. J. IGPL 13(4), 415\u2013433 (2005)","journal-title":"Log. J. IGPL"},{"key":"9253_CR24","unstructured":"HOL4 Website: http:\/\/hol.sourceforge.net\/ (2011). Accessed 1 May 2012"},{"key":"9253_CR25","doi-asserted-by":"crossref","unstructured":"Howe, D.: Equality in lazy computation systems. In: Parikh, R. (ed.) LICS \u201989, pp. 198\u2013203 (1989)","DOI":"10.1109\/LICS.1989.39174"},{"issue":"2","key":"9253_CR26","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0008","volume":"124","author":"D Howe","year":"1996","unstructured":"Howe, D.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103\u2013112 (1996)","journal-title":"Inf. Comput."},{"key":"9253_CR27","unstructured":"Isabelle\/HOL Website: http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/ (2011). Accessed 1 May 2012"},{"key":"9253_CR28","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall International Series in Computer Science. Prentice Hall (1991)"},{"key":"9253_CR29","unstructured":"Kapur, D., Musser, D.R.: Inductive reasoning with incomplete specifications (preliminary report). In: Meyer, A. (ed.) LICS \u201986, pp.\u00a0367\u2013377. IEEE Computer Society (1986)"},{"key":"9253_CR30","unstructured":"Klein, G., Nipkow, T., Paulson, L.: The archive of formal proofs. http:\/\/afp.sf.net (2011). Accessed 1 May 2012"},{"key":"9253_CR31","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, 17\u201320 August 2006, Proceedings. Lecture Notes in Comput. Sci., vol. 4130, pp.\u00a0589\u2013603. Springer (2006)"},{"issue":"4","key":"9253_CR32","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303\u2013336 (2010)","journal-title":"J. Autom. Reason."},{"issue":"7","key":"9253_CR33","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"3","key":"9253_CR34","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I Mason","year":"1991","unstructured":"Mason, I., Talcott, C.L.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 287\u2013327 (1991)","journal-title":"J. Funct. Program."},{"key":"9253_CR35","unstructured":"Morris, J.: Lambda-calculus models of programming languages. Ph.D. thesis, MIT (1968)"},{"key":"9253_CR36","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Lecture Notes in Comput. Sci., vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9253_CR37","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Operationally-based theories of program equivalence. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511526619.007"},{"key":"9253_CR38","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value, and the lambda-calculus. Theor. Comput. Sci. 1, 125\u2013159 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"9253_CR39","unstructured":"Sabel, D., Schmidt-Schau\u00df, M., Harwath, F.: Reasoning about contextual equivalence: from untyped to polymorphically typed calculi. In: Fischer, S., Maehle, E., Reischuk, R. (eds.) INFORMATIK 2009. GI Edition - Lecture Notes in Informatics, vol. 154, pp. 369; 2931\u20132945 (2009)"},{"key":"9253_CR40","doi-asserted-by":"crossref","unstructured":"Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T., Schmidt, D., Sudborough, I. (eds.) The Essence of Computation 2002, pp. 60\u201384. Springer (2002)","DOI":"10.1007\/3-540-36377-7_4"},{"issue":"2","key":"9253_CR41","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1093\/comjnl\/42.2.73","volume":"42","author":"B Schieder","year":"1999","unstructured":"Schieder, B., Broy, M.: Adapting calculational logic to the undefined. Comput. J. 42(2), 73\u201381 (1999)","journal-title":"Comput. J."},{"issue":"7","key":"9253_CR42","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2006.10.038","volume":"174","author":"A Schlosser","year":"2007","unstructured":"Schlosser, A., Walther, C., Gonder, M., Aderhold, M.: Context dependent procedures and computed types in verifun. Electron. Notes Theor. Comput. Sci. 174(7), 61\u201378 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"11\u201313","key":"9253_CR43","doi-asserted-by":"crossref","first-page":"1521","DOI":"10.1016\/j.tcs.2009.12.001","volume":"411","author":"M Schmidt-Schau\u00df","year":"2010","unstructured":"Schmidt-Schau\u00df, M., Sabel, D.: On generic context lemmas for higher-order calculi with sharing. Theor. Comput. Sci. 411(11\u201313), 1521\u20131541 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"9253_CR44","unstructured":"Schmidt-Schau\u00df, M., Sabel, D.: A Termination Proof of Reduction in a Simply Typed Calculus with Constructors. Frank report\u00a042, Inst. f\u00fcr Informatik. Goethe-Universit\u00e4t Frankfurt (2010)"},{"issue":"12\u201313","key":"9253_CR45","doi-asserted-by":"crossref","first-page":"1217","DOI":"10.1016\/j.tcs.2008.11.020","volume":"410","author":"L Schr\u00f6der","year":"2009","unstructured":"Schr\u00f6der, L., Mossakowski, T.: HasCasl: integrated higher-order specification and program development. Theor. Comput. Sci. 410(12\u201313), 1217\u20131260 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"9253_CR46","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","volume":"121","author":"D Scott","year":"1993","unstructured":"Scott, D.: A type-theoretical alternative to CUCH, ISWIM, OWHY. Theor. Comput. Sci. 121, 411\u2013440 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"9253_CR47","unstructured":"VeriFun Website: www.inferenzsysteme.informatik.tu-darmstadt.de\/verifun\/ (2011). Accessed 1 May 2012"},{"key":"9253_CR48","doi-asserted-by":"crossref","unstructured":"Walther, C.: Mathematical induction. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 127\u2013228. Oxford University Press (1994)","DOI":"10.1093\/oso\/9780198537465.003.0003"},{"key":"9253_CR49","doi-asserted-by":"crossref","unstructured":"Walther, C., Schweitzer, S.: Reasoning about incompletely defined programs. In: Sutcliffe, G., Voronkov, A. (eds.) Proc. LPAR \u201905. Lecture Notes in Comput. Sci., vol. 3835, pp. 427\u2013442 (2005)","DOI":"10.1007\/11591191_30"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9253-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9253-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9253-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T01:11:28Z","timestamp":1743297088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9253-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,8]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["9253"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9253-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2012,6,8]]}}}