{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T01:37:22Z","timestamp":1750469842364},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617808"},{"type":"electronic","value":"9783540707226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_69","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:26Z","timestamp":1330295126000},"page":"165-182","source":"Crossref","is-referenced-by-count":11,"title":["A natural deduction approach to dynamic logic"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"4","key":"12_CR1","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"K. R. Apt. Ten years of Hoare's logic: A survey \u2014part I. ACM Transactions on Programming Languages and Syms, 3(4):431\u2013483, Oct. 1981.","journal-title":"ACM Transactions on Programming Languages and Syms"},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"A. Avron. Simple consequence relations. Inform. Comput., 92:105\u2013139, Jan. 1991.","journal-title":"Inform. Comput."},{"key":"12_CR3","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"A. Avron, F. Honsell, I. A. Mason, and R. Pollack. Using Typed Lambda Calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309\u2013354, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"R. Burstall and F. Honsell. Operational semantics in a natural deduction setting. In Huet and Plotkin [13], pages 185\u2013214.","DOI":"10.1017\/CBO9780511569807.009"},{"key":"12_CR5","first-page":"95","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Control, 76:95\u2013120, 1988.","journal-title":"Information and Control"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. Mechanizing program logics in higher order logic. In P. A. Subrahmanyam and G. Birtwistle, editors, Current Trends in Hardware Verification and Automated Theorem Prover, pages 387\u2013439. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"D. Harel. First-Order Dynamic Logic. No.68 in LNCS. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09237-4"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"D. Harel. Dynamic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, pages 497\u2013604. Reidel, 1984.","DOI":"10.1007\/978-94-009-6259-0_10"},{"issue":"1","key":"12_CR9","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. ACM, 40(1):143\u2013184, Jan. 1993.","journal-title":"J. ACM"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"M. Heisel, W. Reif, and W. Stephan. A dynamic logic for program verification. In A. Meyer and M. Taitslin, editors, Proc. of LFCS (Logic at Botik), number 363 in Lecture Notes in Computer Science, pages 134\u2013145. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51237-3_12"},{"key":"12_CR11","unstructured":"F. Honsell and M. Miculan. Encoding program logics in type theories. In J. Despeyroux, editor, Deliverables of the TYPES Workshop Proving Properties of Programming Languages, Sophia-Antipolis, Sept. 1993."},{"key":"12_CR12","unstructured":"F. Honsell, M. Miculan, and C. Paravano. Encoding modal logics in Logical Frameworks. To appear, 1996."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"G. Huet and G. Plotkin, editors. Logical Frameworks. CUP, June 1990.","DOI":"10.1017\/CBO9780511569807"},{"key":"12_CR14","unstructured":"INRIA, Rocquencourt. The Coq Proof Assistant Reference Manual, July 1995."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"D. Kozen and J. Tiuryn. Logics of Programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 789\u2013840. North Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50019-6"},{"key":"12_CR16","unstructured":"Z. Luo, R. Pollack, and P. Taylor. How to use LEGO (A Preliminary User's Manual). Department of Computer Science, University of Edinburgh, Oct. 1989."},{"issue":"2","key":"12_CR17","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/322307.322324","volume":"29","author":"A. R. Meyer","year":"1982","unstructured":"A. R. Meyer and J. Y. Halpern. Axiomatic definition of programming languages: A theoretical assessment. J. ACM, 29(2):555\u2013576, Apr. 1982.","journal-title":"J. ACM"},{"key":"12_CR18","first-page":"299","volume-title":"number 596 in LNAI","author":"S. Michaylov","year":"1991","unstructured":"S. Michaylov and F. Pfenning. Natural Semantics and some of its Meta-Theory in Elf. In L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, number 596 in LNAI, pages 299\u2013344, Stockolm, Sweden, Jan. 1991. Springer-Verlag."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"M. Miculan. The expressive power of structural operational semantics with explicit assumptions. In H. Barendregt and T. Nipkow, editors, Proceedings of TYPES'93, number 806 in LNCS, pages 292\u2013320. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58085-9_80"},{"key":"12_CR20","unstructured":"M. Miculan. Encoding Logical Theories of Programs. PhD thesis, Universit\u00e0 di Pisa, 1997. To appear."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313\u2013322. IEEE, June 1989.","DOI":"10.1109\/LICS.1989.39186"},{"key":"12_CR22","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"W. Reif. The KIV system: Systematic construction of verified software. In D. Kapur, editor, Proc. of CADE-11, number 607 in Lecture Notes in Computer Science, pages 753\u2013757. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_218"},{"key":"12_CR24","first-page":"39","volume-title":"Syntactic control of interference","author":"J. C. Reynolds","year":"1978","unstructured":"J. C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39\u201346, Tucson, Oct. 1978. The Association for Computing Machinery."},{"key":"12_CR25","unstructured":"C. Stirling. Logics for While Programs: Algorithmic\/Dynamic Logics. Unpublished notes, 1985."},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"C. Stirling. Modal and Temporal Logics. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 477\u2013563. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"12_CR27","unstructured":"B. Werner. Une th\u00e9orie des constructions inductives. PhD thesis, Universit\u00e9 Paris 7, 1994."}],"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-61780-9_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:47:21Z","timestamp":1713635241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}