{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:19:25Z","timestamp":1725495565709},"publisher-location":"Berlin, Heidelberg","reference-count":62,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540563204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-56320-2_55","type":"book-chapter","created":{"date-parts":[[2007,11,19]],"date-time":"2007-11-19T05:53:33Z","timestamp":1195451613000},"page":"103-127","source":"Crossref","is-referenced-by-count":0,"title":["Formal theories and software systems: Fundamental connections between Computer Science and Logic"],"prefix":"10.1007","author":[{"given":"Robert L.","family":"Constable","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"M. Aagaard and M. Leeser. Verifying a logic synthesis tool in Nuprl. In G. Bochmann and D. Probst, editors, Participants copy of Proceedings of Workshop on Computer-Aided. Verification, pages 72\u201383. Springer-Verlag, June 1992. To appear by Springer-Verlag, 1993."},{"key":"7_CR2","unstructured":"S. Abramsky. Computational interpretations of linear logic. TCS, 1992. To appear."},{"key":"7_CR3","unstructured":"W. Aitken and R. C. Constable. Reflecting on Nuprl Lessons 1\u20134. Technical report, Cornell University, Computer Science Dept., 1992. To appear."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"S. Allen, R. Constable, D. Howe, and W. Aitken. The semantics of reflected proof. Proc. of Fifth Symp. on Logic in Comp. Sci., IEEE, pages 95\u2013197, June 1990.","DOI":"10.1109\/LICS.1990.113737"},{"key":"7_CR5","unstructured":"S. F. Allen. A non-type-theoretic definition of Martin-L\u00f6f's types. Proc. of Second Symp. on Logics in Computer Science, IEEE, pages 215\u2013224., June 1987."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"A. Appel. Compiling with Continuations. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511609619"},{"key":"7_CR7","first-page":"101","volume-title":"An environment for automated reasoning about partial functions","author":"D. Basin","year":"1988","unstructured":"D. Basin. An environment for automated reasoning about partial functions. In 9th International Conference on Automated Deduction, pages 101\u2013110. Springer-Verlag, NY, 1988."},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0167-9260(91)90048-P","volume":"11","author":"D. Basin","year":"1991","unstructured":"D. Basin, G. Brown, and M. Leeser. Formally Verified Synthesis of Combinational CMOS Circuits. Integration: The International Journal of VLSI Design, 11:235\u2013250, 1991.","journal-title":"Integration: The International Journal of VLSI Design"},{"key":"7_CR9","first-page":"53","volume-title":"Intuitionism and Proof Theory","author":"E. Bishop","year":"1970","unstructured":"E. Bishop. Mathematics as a Numerical Language. In Intuitionism and Proof Theory., pages 53\u201371. North-Holland, NY, 1970."},{"key":"7_CR10","unstructured":"W. W. Bledsoe. A new method for proving certain Presburger formulas. Fourth IJCAI, September 1975. Tblisi, USSR."},{"key":"7_CR11","volume-title":"Elements of Mathematics, Algebra, Volume 1","author":"N. Bourbaki","year":"1968","unstructured":"N. Bourbaki. Elements of Mathematics, Algebra, Volume 1. Addison-Wesley, Reading, MA, 1968."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"W. Chen. Tactic-based theorem proving and knowledge-based forward chaining. In D. Kapur, editor, Eleventh International Conference on Automated Deduction, pages 552\u2013566. Springer-Verlag, June 1992.","DOI":"10.1007\/3-540-55602-8_191"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"J. Chirimar and D. Howe. Implementing constructive real analysis: a preliminary report. In Symposium on Constructivity in Computer Science. Springer-Verlag, 1991. To appear.","DOI":"10.1007\/BFb0021090"},{"key":"7_CR14","unstructured":"R. C. Cleaveland. Type-Theoretic Models of Concurrency. PhD thesis, Cornell University, 1987."},{"key":"7_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11492-0","volume-title":"Introduction to the PL\/CV2 Programming Logic, LNCS, volume 135","author":"R. Constable","year":"1982","unstructured":"R. Constable, S. Johnson, and C. Eichenlaub. Introduction to the PL\/CV2 Programming Logic, LNCS, volume 135. Springer-Verlag, NY, 1982."},{"issue":"3","key":"7_CR16","first-page":"285","volume":"1","author":"R. Constable","year":"1984","unstructured":"R. Constable, T. Knoblock, and J. Bates. Writing programs that construct proofs. J. Automated Reasoning, 1(3):285\u2013326, 1984.","journal-title":"J. Automated Reasoning"},{"key":"7_CR17","unstructured":"R. L. Constable. Constructive mathematics and automatic program writers. In Proc. IFP Congr., pages 229\u201333, Ljubljana, 1971."},{"key":"7_CR18","unstructured":"R. L. Constable. Lectures on: Classical proofs as programs. NATO ASI Series, Constructive Methods of Computing Science, F, 1991."},{"key":"7_CR19","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986."},{"key":"7_CR20","first-page":"45","volume-title":"Formal Techniques in Artificial Intelligence: A Source Book","author":"R. L. Constable","year":"1990","unstructured":"R. L. Constable and D. J. Howe. Implementing metamathematics as an approach to automatic theorem proving. In R. Banerji, editor, Formal Techniques in Artificial Intelligence: A Source Book, pages 45\u201376. Elsevier Science Publishers (North-Holland), 1990."},{"key":"7_CR21","first-page":"151","volume-title":"The complexity of theorem proving procedures","author":"S. Cook","year":"1971","unstructured":"S. Cook. The complexity of theorem proving procedures. In Proc. of the 3rd ACM Symposium on Theory of Computation, pages 151\u2013158. ACM, NY, 1971."},{"key":"7_CR22","volume-title":"Combinatory Logic, Vol. 1","author":"H. Curry","year":"1968","unstructured":"H. Curry, R. Feys, and W. Craig. Combinatory Logic, Vol. 1. Amsterdam:North-Holland, 1968."},{"key":"7_CR23","first-page":"1","volume-title":"Automation of Reasoning 1","author":"M. Davis","year":"1983","unstructured":"M. Davis. The prehistory and early history of automated deduction. In Automation of Reasoning 1, pages 1\u201328. Springer-Verlag, NY, 1983."},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0060623","volume":"125","author":"N. deBruijn","year":"1968","unstructured":"N. deBruijn. The mathematical language Automath, its usage and, some of its extensions. Symp. on Automatic Demonstration, Lecture Notes in Math, 125:29\u201361, 1968.","journal-title":"Symp. on Automatic Demonstration, Lecture Notes in Math"},{"key":"7_CR25","unstructured":"N. deBruijn. A survey of the project Automath. In To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism., pages 589\u2013606. Academic Press, 1980."},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"S. Feferman. A language and axioms for explicit mathematics. In Algebra and Logic, Lecture Notes in Mathematics, pages 87\u2013139. Springer-Verlag, 1975.","DOI":"10.1007\/BFb0062852"},{"key":"7_CR27","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1090\/conm\/106\/1057818","volume":"106","author":"S. Feferman","year":"1990","unstructured":"S. Feferman. Polymorphic typed lambda-calculi in a type free axiomatic framework. Contemporary Mathematics, 106:101\u2013135, 1990.","journal-title":"Contemporary Mathematics"},{"key":"7_CR28","first-page":"1","volume-title":"From Frege to Godel: A Source Book in Mathematical Logic, 1879\u20131931","author":"G. Frege","year":"1967","unstructured":"G. Frege. Begriffsschrift, a formula language, modeled upon that for arithmetic for pure thought. In From Frege to Godel: A Source Book in Mathematical Logic, 1879\u20131931, pages 1\u201382. Harvard University Press, Cambridge, Mass., 1967."},{"key":"7_CR29","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0049-237X(08)70843-7","volume-title":"2nd Scandinavian Logic Symp.","author":"J.-Y. Girard","year":"1971","unstructured":"J.-Y. Girard. Une extension de l'interpretation de godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In 2nd Scandinavian Logic Symp., pages 63\u201369. Springer-Verlag, NY, 1971."},{"key":"7_CR30","unstructured":"J.-Y. Girard. On the unity of logic. In Proceedings of Computer and Systems Sciences, NATO Advanced Science Institute Series F, 1991."},{"key":"7_CR31","unstructured":"K. G\u00f6del. On intuitionistic arithmetic and number theory. In M. Davis, editor, The Undecidable, pages 75\u201381. Raven Press, 1965."},{"key":"7_CR32","unstructured":"M. Gordon. HOL: A machine oriented formalization of higher order logic. Technical Report 68, Cambridge University, 1985."},{"key":"7_CR33","volume-title":"volume 78 of Lecture Notes in Computer Science","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: a mechanized logic of computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, NY, 1979."},{"key":"7_CR34","volume-title":"Feasible Computations and Provable Complexity Properties","author":"J. Hartmanis","year":"1978","unstructured":"J. Hartmanis. Feasible Computations and Provable Complexity Properties. SIAM, Philadelphia, PA, 1978."},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2307\/1994208","volume":"117","author":"J. Hartmanis","year":"1965","unstructured":"J. Hartmanis and R. Stearns. On the computational complexity of algorithms. Transactions of the American Mathematics Society, 117:285\u2013306, 1965.","journal-title":"Transactions of the American Mathematics Society"},{"key":"7_CR36","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"W. Howard","year":"1980","unstructured":"W. Howard. The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479\u2013490. Academic Press, NY, 1980."},{"key":"7_CR37","unstructured":"D. Howe. The computational behaviour of Girard's paradox. Proc. of Second Symp. on Logic in Comp. Sci., IEEE, pages 205\u2013214, June 1987."},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"D. Howe. Implementing number theory: An experiment with Nuprl. 8th International Conference on Automated Deduction, pages 404\u2013415, July 1987.","DOI":"10.1007\/3-540-16780-3_108"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"D. Howe. Equality in lazy computation systems. In Proc. of Second Symp. on Logic in Comp. Sci., pages 198\u2013203. IEEE Computer Society, June 1989.","DOI":"10.1109\/LICS.1989.39174"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"D. Howe. A simple type theory for reasoning about functional programs. pre print, 1992.","DOI":"10.1007\/3-540-56883-2_9"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"D. Howe. Reasoning about functional programs in Nuprl. Functional Programming, Concurrency, Simulation and Automated Reasoning, LNCS, 1993. To appear.","DOI":"10.1007\/3-540-56883-2_9"},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"G. Huet. Theorem proving systems of the Formel project. In Proc. of the 8th International Conference on Automated Deduction, Lecture Notes in Computer Science, pages 687\u2013688. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16780-3_138"},{"key":"7_CR43","unstructured":"G. Huet. A uniform approach to type theory. In G. Huet, editor, Logical Foundations of Functional Programming, pages 337\u2013398. Addison-Wesley, 1990."},{"key":"7_CR44","first-page":"311","volume-title":"Proceedings of the IFIP TC10\/WG10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience","author":"P. B. Jackson","year":"1992","unstructured":"P. B. Jackson. Nuprl and its use in circuit design. In V. Stavridou, T. Melham, and R. Boute, editors, Proceedings of the IFIP TC10\/WG10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 311\u2013336. North-Holland, The Netherlands, June 1992."},{"key":"7_CR45","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"S. C. Kleene. Introduction to Metamathematics. D. Van Nostrand, Princeton, 1952."},{"key":"7_CR46","first-page":"1","volume":"1","author":"A. Kolmogorov","year":"1965","unstructured":"A. Kolmogorov. Three approaches to the concept of 'the amount of information'. Probl. Inf. Tramsm., 1:1\u20137, 1965.","journal-title":"Probl. Inf. Tramsm."},{"key":"7_CR47","volume-title":"Technical Report TR 86-779","author":"C. Kreitz","year":"1986","unstructured":"C. Kreitz. Constructive automata theory implemented with the Nuprl proof development system. Technical Report TR 86-779, Cornell University, Ithaca, New York, September 1986."},{"key":"7_CR48","first-page":"227","volume-title":"Intuitionism and Proof Theory","author":"H. Lauchli","year":"1970","unstructured":"H. Lauchli. An abstract notion of realizability for which intuitionistic predicate calculus is complete. In Intuitionism and Proof Theory., pages 227\u201334. North-Holland, Amsterdam, 1970."},{"key":"7_CR49","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1098\/rsta.1992.0025","volume":"339","author":"M. Leeser","year":"1992","unstructured":"M. Leeser. Using Nuprl for the verification and synthesis of hardware. Phil. Trans. R. Soc. Lond., 339:49\u201368, 1992.","journal-title":"Phil. Trans. R. Soc. Lond."},{"key":"7_CR50","volume-title":"Logical Papers: A Selection","author":"G. Leibniz","year":"1966","unstructured":"G. Leibniz. Logical Papers: A Selection. Clarendon Press, Oxford, 1966."},{"key":"7_CR51","first-page":"115","volume":"9","author":"L. Levin","year":"1973","unstructured":"L. Levin. Universal search problems. Problemy Peredaci Informacii 9, pages 115\u2013116, 1973.","journal-title":"Problemy Peredaci Informacii"},{"key":"7_CR52","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Sixth International Congress for Logic, Methodology, and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"P. Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u201375. North-Holland, Amsterdam, 1982."},{"key":"7_CR53","volume-title":"ONTIC: A Knowledge Representation System for Mathematics","author":"D. A. McAllester","year":"1989","unstructured":"D. A. McAllester. ONTIC: A Knowledge Representation System for Mathematics. MIT Press, Cambrige, Mass., 1989."},{"key":"7_CR54","first-page":"219","volume-title":"Proceedings of the Symposium in Pure Math, Recursive Function Theory, Vol V","author":"J. McCarthy","year":"1962","unstructured":"J. McCarthy. Computer programs for checking mathematical proofs. In Proceedings of the Symposium in Pure Math, Recursive Function Theory, Vol V, pages 219\u2013228. AMS, Providence, RI, 1962."},{"key":"7_CR55","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, part 1. Technical Report CSR-302-89, LFCS, University of Edinburgh, June 1989."},{"key":"7_CR56","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1991."},{"key":"7_CR57","doi-asserted-by":"crossref","unstructured":"C. Murthy. An evaluation semantics for classical proofs. In LICS, '91, pages 96\u2013107, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151634"},{"key":"7_CR58","volume-title":"Programming in Martin-Lof 's Type Theory","author":"B. Nordstrom","year":"1990","unstructured":"B. Nordstrom, K. Petersson, and J. Smith. Programming in Martin-Lof 's Type Theory. Oxford Sciences Publication, Oxford, 1990."},{"key":"7_CR59","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F\u2032ws programs from proofs in the calculus of constructions. In Proceedings of POPL, 1989.","DOI":"10.1145\/75277.75285"},{"key":"7_CR60","doi-asserted-by":"publisher","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B. Russell","year":"1908","unstructured":"B. Russell. Mathematical logic as based on a theory of types. Am. J. Math., 30:222\u201362, 1908.","journal-title":"Am. J. Math."},{"issue":"4","key":"7_CR61","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF00244278","volume":"1","author":"N. Shankar","year":"1985","unstructured":"N. Shankar. Towards mechanical metamathematics. J. Automated Reasoning, 1(4):407\u2013434, 1985.","journal-title":"J. Automated Reasoning"},{"key":"7_CR62","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. Shostak","year":"1979","unstructured":"R. Shostak. A practical decision procedure for arithmetic with function symbols. JACM, 26:351\u2013360, 1979.","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Future Tendencies in Computer Science, Control and Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56320-2_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:03:20Z","timestamp":1605629000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56320-2_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540563204"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/3-540-56320-2_55","relation":{},"subject":[]}}