{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:17Z","timestamp":1761611117851,"version":"3.41.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1023\/a:1026748613865","type":"journal-article","created":{"date-parts":[[2003,11,6]],"date-time":"2003-11-06T18:09:07Z","timestamp":1068142147000},"page":"205-221","source":"Crossref","is-referenced-by-count":20,"title":["The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction"],"prefix":"10.1007","volume":"26","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Schwichtenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Monika","family":"Seisenberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"316995_CR1","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J. L. Bates","year":"1985","unstructured":"Bates, J. L. and Constable, R. L.: Proofs as programs, ACM Trans. Programming Languages and Systems\n7(1) (1985), 113\u2013136.","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"316995_CR2","series-title":"Appl. Logic Series","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-94-017-0435-9_2","volume-title":"Automated Deduction-A Basis for Applications, Vol. II: Systems and Implementation Techniques","author":"H. Benl","year":"1998","unstructured":"Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., and Zuber, W.: Proof theory at work: Program development in the Minlog system, in W. Bibel and P. Schmitt (eds), Automated Deduction-A Basis for Applications, Vol. II: Systems and Implementation Techniques, Appl. Logic Series, Kluwer Academic Publishers, Dordrecht, 1998, pp. 41\u201371."},{"key":"316995_CR3","series-title":"Computer and Systems Sci. Series F","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-642-58622-4_4","volume-title":"Computational Logic","author":"H. Benl","year":"1999","unstructured":"Benl, H. and Schwichtenberg, H.: Formal correctness proofs of functional programs: Dijkstra's algorithm, a case study, in U. Berger and H. Schwichtenberg (eds), Computational Logic, Computer and Systems Sci. Series F 165, Springer-Verlag, Berlin, 1999, pp. 113\u2013126."},{"key":"316995_CR4","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BFb0037100","volume-title":"Typed Lambda Calculi and Applications","author":"U. Berger","year":"1993","unstructured":"Berger, U.: Program extraction from normalization proofs, in M. Bezem and J. Groote (eds), Typed Lambda Calculi and Applications, Lecture Notes in Comput. Sci. 165, Springer-Verlag, Berlin, 1993, pp. 91\u2013106."},{"key":"316995_CR5","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-60178-3_80","volume-title":"Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, IN, USA, October 1994","author":"U. Berger","year":"1995","unstructured":"Berger, U. and Schwichtenberg, H.: Program extraction from classical proofs, in D. Leivant (ed.), Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, IN, USA, October 1994, Lecture Notes in Comput. Sci. 960, Springer-Verlag, Berlin, 1995, pp. 77\u201397."},{"issue":"1","key":"316995_CR6","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/TSE.1981.230815","volume":"7","author":"M. Broy","year":"1981","unstructured":"Broy, M. and Pepper, P.: Program development as a formal activity, IEEE Trans. on Software Eng.\n7(1) (1981), 14\u201322.","journal-title":"IEEE Trans. on Software Eng."},{"key":"316995_CR7","series-title":"Lecture Notes in Comput. Sci.","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1999","unstructured":"Coquand, T. and Persson, H.: Gr\u00f6bner bases in type theory, in T. Altenkirch, W. Naraschewski, and B. Reus (eds), Types for Proofs and Programs, Lecture Notes in Comput. Sci. 1657, Springer-Verlag, Berlin, 1999."},{"key":"316995_CR8","doi-asserted-by":"crossref","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"L. Dickson","year":"1913","unstructured":"Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors, Amer. J. Math.\n35 (1913), 413\u2013422.","journal-title":"Amer. J. Math."},{"key":"316995_CR9","unstructured":"Dragalin, A.: New kinds of realizability, in Abstracts of the 6th International Congress of Logic, Methodology and Philosophy of Sciences, Hannover, Germany, 1979, pp. 20\u201324."},{"key":"316995_CR10","series-title":"Lecture Notes in Math.","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BFb0103100","volume-title":"Higher Set Theory","author":"H. Friedman","year":"1978","unstructured":"Friedman, H.: Classically and intuitionistically provably recursive functions, in D. Scott and G. M\u00fcller (eds), Higher Set Theory, Lecture Notes in Math. 669, Springer-Verlag, Berlin, 1978, pp. 21\u201328."},{"key":"316995_CR11","doi-asserted-by":"crossref","unstructured":"Kohlenbach, U.: Analysing proofs in analysis, in W. Hodges, M. Hyland, C. Steinhorn, and J. Truss (eds), Logic: From Foundations to Applications. European Logic Colloquium (Keele, 1993), Oxford University Press, 1996, pp. 225\u2013260.","DOI":"10.1093\/oso\/9780198538622.003.0010"},{"key":"316995_CR12","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types, in A. Heyting (ed.), Constructivity in Mathematics, North-Holland, Amsterdam, 1959, pp. 101\u2013128."},{"issue":"3","key":"316995_CR13","doi-asserted-by":"crossref","first-page":"682","DOI":"10.2307\/2274322","volume":"50","author":"D. Leivant","year":"1985","unstructured":"Leivant, D.: Syntactic translations and provably recursive functions, J. Symbolic Logic\n50(3) (1985), 682\u2013688.","journal-title":"J. Symbolic Logic"},{"key":"316995_CR14","series-title":"Technical Report 90\u20131151","volume-title":"Extracting constructive content from classical proofs","author":"C. Murthy","year":"1990","unstructured":"Murthy, C.: Extracting constructive content from classical proofs, Technical Report 90\u20131151, Dept. of Comp. Science, Cornell Univ., Ithaca, New York. PhD thesis, 1990."},{"key":"316995_CR15","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. S. J. A. Nash-Williams","year":"1963","unstructured":"Nash-Williams, C. S. J. A.: On well-quasi-ordering finite trees, Proc. Cambridge Philos. Soc.\n59 (1963), 833\u2013835.","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"316995_CR16","series-title":"Contemp. Math.","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1090\/conm\/106\/1057826","volume-title":"Logic and Computation","author":"F. Pfenning","year":"1990","unstructured":"Pfenning, F.: Program development through proof transformation, in W. Sieg (ed.), Logic and Computation, Contemp. Math. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 251\u2013262."},{"issue":"2","key":"316995_CR17","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"Tait, W. W.: Intensional interpretations of functionals of finite type I, J. Symbolic Logic\n32(2) (1967), 198\u2013212.","journal-title":"J. Symbolic Logic"},{"key":"316995_CR18","series-title":"Lecture Notes in Math.","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066739","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","author":"A. S. Troelstra","year":"1973","unstructured":"Troelstra, A. S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Math. 344, Springer-Verlag, Berlin, 1973."},{"key":"316995_CR19","unstructured":"Troelstra, A. S. and van Dalen, D.: Constructivism in Mathematics: An Introduction, Stud. Logic Found. Math. 121, 123, North-Holland, Amsterdam, 1988."},{"key":"316995_CR20","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1112\/jlms\/s2-47.2.193","volume":"47","author":"W. Veldman","year":"1993","unstructured":"Veldman, W. and Bezem, M.: Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics, J. London Math. Soc.\n47 (1993), 193\u2013211.","journal-title":"J. London Math. Soc."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026748613865.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1026748613865\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026748613865.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:33:29Z","timestamp":1749123209000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1026748613865"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["316995"],"URL":"https:\/\/doi.org\/10.1023\/a:1026748613865","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}