{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:55Z","timestamp":1725467515141},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055132","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"105-122","source":"Crossref","is-referenced-by-count":5,"title":["Classical propositional decidability via Nuprl proof extraction"],"prefix":"10.1007","author":[{"given":"James L.","family":"Caldwell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"7_CR1","unstructured":"Stuart F. Allen. From dy\/dx to []P: A matter of notation. In Proceedings of User Interfaces for Theorem Provers 1998. Eindhoven University of Technology, July 1998."},{"key":"7_CR2","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. NY:Academic Press, 1979."},{"key":"7_CR3","unstructured":"James Caldwell. Extracting propositional decidability: A proof of prepositional decidability in constructive type theory and its extract. Available at http:\/\/simon.cs.cornell.edu\/Info\/People\/caldwell\/papers.html, March 1997."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"James Caldwell. Moving proofs-as-programs into practice. In Proceedings, 12th IEEE International Conference Automated Software Engineering. IEEE Computer Society, 1997.","DOI":"10.1109\/ASE.1997.632819"},{"key":"7_CR5","volume-title":"Formal Techniques in Artificial Intelligence: A Source Book.","author":"R. Constable","year":"1990","unstructured":"R. Constable and D. Howe. Implementing metamathematics as an approach to automatic theorem proving. In R.B. Banerji, editor, Formal Techniques in Artificial Intelligence: A Source Book. Elsevier Science Publishers (North-Holland), 1990."},{"volume-title":"Implementing Mathematics with the Nuprl Proof Development System","year":"1986","key":"7_CR6","unstructured":"Robert L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"7_CR7","volume-title":"Technical Report 12","author":"M. Davis","year":"1977","unstructured":"M. Davis and J. Schwartz. Metamathematical extensibility for theorem verifiers and proof checkers. Technical Report 12, Courant Institute of Mathematical Sciences, New York, 1977."},{"key":"7_CR8","unstructured":"Michael J. C. Gordon and Tom F. Melham. Introduction to HOL. Cambridge University Press, 1993."},{"key":"7_CR9","volume-title":"Technical Report CRC-053","author":"J. Harrison","year":"1995","unstructured":"John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995."},{"key":"7_CR10","first-page":"701","volume-title":"volume 526 of Lecture Notes in Computer Science","author":"S. Hayashi","year":"1991","unstructured":"Susumu Hayashi. Singleton, union, and intersection types for program extraction. In Proceedings of the International Conference on Theoretical Aspects of Computer Software TACS'91, volume 526 of Lecture Notes in Computer Science, pages 701\u2013730, Berlin, 1991. Springer Verlag."},{"key":"7_CR11","volume-title":"Foundations of Computing","author":"S. Hayashi","year":"1988","unstructured":"Susumu Hayashi and Hiroshi Nakano. PX: A Computational Logic. Foundations of Computing. MIT Press, Cambridge, MA, 1988."},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/BF01245632","volume":"3","author":"M. Hedberg","year":"1991","unstructured":"M. Hedberg. Normalising the associative law: An experiment with Martin-L\u00f6f's type theory. Formal Aspects of Computing, 3:218\u2013252, 1991.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR13","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"Stephen C. Kleene. Introduction to Metamathematics. van Nostrand, Princeton, 1952."},{"key":"7_CR14","first-page":"170","volume-title":"volume 87 of Lecture Notes in Computer Science","author":"J. Leszczylowski","year":"1981","unstructured":"J. Leszczylowski. An experiment with Edinburgh LCF. In W. Bibel and R. Kowalski, editors, 5th International Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 170\u2013181, New York, 1981. Springer-Verlag."},{"issue":"5\u20136","key":"7_CR15","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15(5\u20136):607\u2013640, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BF00246023","volume":"2","author":"L. Paulson","year":"1986","unstructured":"Lawrence Paulson. Proving termination of normalization functions for conditional expressions. Journal of Automated Reasoning, 2:63\u201374, 1986.","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"7_CR17","first-page":"407","volume":"1","author":"N. Shanker","year":"1985","unstructured":"N. Shanker. Towards mechanical metamathematics. Journal of Automated Reasoning, 1(4):407\u2013434, 1985.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055132","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T13:46:00Z","timestamp":1549892760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055132"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0055132","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}