{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:22Z","timestamp":1774837822035,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540432876","type":"print"},{"value":"9783540458425","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_2","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T20:00:38Z","timestamp":1180209638000},"page":"24-40","source":"Crossref","is-referenced-by-count":53,"title":["Executing Higher Order Logic"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Berghofer","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, editors, Theorem Proving in Higher Order Logics, 12th International Conference (TPHOLs\u201999), volume 1690 of Lect. Notes in Comp. Sci., pages 323\u2013340. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48256-3_22"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"J. H. Andrews. Executing formal specifications by translation to higher order logic programming. In E. L. Gunter and A. Felty, editors, 10th International Conference on Theorem Proving in Higher Order Logics, volume 1275 of Lect. Notes in Comp. Sci., pages 17\u201332. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0028383"},{"key":"2_CR3","unstructured":"I. Attali, D. Caromel, and M. Russo. A formal and executable semantics for Java. In Proceedings of Formal Underpinnings of Java, an OOPSLA\u201998 Workshop, Vancouver, Canada, 1998. Technical report, Princeton University."},{"key":"2_CR4","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, H. Laulh\u00e8re, C. Mu\u00f1oz, C. Murthy, C. Parent-Vigouroux, P. Loiseleur, C. Paulin-Mohring, A. Sa\u03cabi, and B. Werner. The Coq proof assistant reference manual-version 6.3.1. Technical report, INRIA, 1999."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"D. Basin. Lazy infinite-state analysis of security protocols. In Secure Networking \u2014 CQRE [Secure]\u2019 99, volume 1740 of Lect. Notes in Comp. Sci., pages 30\u201342. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-46701-7_3"},{"key":"2_CR6","unstructured":"T. Despeyroux. Typol: a formalism to implement natural semantics. Technical Report 94, INRIA, 1988."},{"key":"2_CR7","unstructured":"C. Dubois and R. Gayraud. Compilation de la s\u00e9mantique naturelle vers ML. In Proceedings of journ\u00e9es francophones des langages applicatifs (JFLA99), 1999. Available via http:\/\/pauillac.inria.fr\/~weis\/jfla99\/ps\/dubois.ps ."},{"key":"2_CR8","unstructured":"W. Goerigk, July 2000. Personal communication."},{"key":"2_CR9","unstructured":"M. Hanus, H. Kuchen, and J. Moreno-Navarro. Curry: A truly functional logic language. In Proc. ILPS\u201995 Workshop on Visions for the Future of Logic Programming, pages 95\u2013107, 1995."},{"key":"2_CR10","unstructured":"I. Jacobs and L. Rideau-Gallot. A Centaur tutorial. Technical Report 140, INRIA Sophia-Antipolis, July 1992."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, June 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"2_CR12","unstructured":"C. S. Mellish. The automatic generation of mode declarations for Prolog programs. Technical Report 163, Department of Artificial Intelligence, University of Edinburgh, August 1981."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"T. Nipkow. More Church-Rosser proofs (in Isabelle\/HOL). Journal of Automated Reasoning, 26, 2001.","DOI":"10.1023\/A:1006496715975"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"D. v. Oheimb and T. Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci., pages 119\u2013156. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48737-9_4"},{"key":"2_CR15","unstructured":"S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS System Guide version 2.3. Technical report, SRI International Computer Science Laboratory, Menlo Park CA, September 1999."},{"key":"2_CR16","doi-asserted-by":"publisher","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:607\u2013640, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR17","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. C. Paulson","year":"1998","unstructured":"L. C. Paulson. The inductive approach to verifying cryptographic protocols. J. Computer Security, 6:85\u2013128, 1998.","journal-title":"J. Computer Security"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logic programming in the LF Logical Framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 66\u201378. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"P. S. Rajan. Executing HOL specifications: Towards an evaluation semantics for classical higher order logic. In L. J. M. Claesen and M. J. C. Gordon, editors, Higher order Logic Theorem Proving and its Applications, Leuven, Belgium, September 1992. Elsevier.","DOI":"10.1016\/B978-0-444-89880-7.50039-5"},{"key":"2_CR20","unstructured":"K. Slind. Reasoning about Terminating Functional Programs. PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1999."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:03:00Z","timestamp":1556434980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}