{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:13:51Z","timestamp":1725664431206},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592938"},{"type":"electronic","value":"9783540492337"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59293-8_218","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:12:07Z","timestamp":1330258327000},"page":"531-545","source":"Crossref","is-referenced-by-count":8,"title":["Reasoning with executable specifications"],"prefix":"10.1007","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[]},{"given":"Ranan","family":"Fraer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"35_CR1","volume-title":"Programming Language Implementation and Logic Programming","author":"I. Attali","year":"1988","unstructured":"I. Attali. Compiling Typol with Attribute Grammars. In Programming Language Implementation and Logic Programming, Orl\u00e9ans, France, 1988. Springer Verlag, LNCS."},{"key":"35_CR2","unstructured":"G. Berry. Real-time programming: General purpose or special-purpose languages. In G. Ritter, editor, Information Processing 89, pages 11\u201317. Elsevier Science Publishers P.V, 1989."},{"key":"35_CR3","volume-title":"PhD thesis","author":"Y. Bertot","year":"1991","unstructured":"Y. Bertot. Une Automatisation du Calcul des R\u00e9sidus en S\u00e9mantique Naturelle. PhD thesis, Universit\u00e9 de Nice-Sophia Antipolis, 1991."},{"key":"35_CR4","unstructured":"Y. Bertot, G. Kahn, and L. Th\u00e9ry. Real Theorem Provers Deserve Real Interfaces. In 5th ACM Symposium on Software Development Environments, Washington, 1992. Also available as INRIA Research Report, RR-1684."},{"key":"35_CR5","volume-title":"PhD thesis","author":"K. Buth","year":"1994","unstructured":"K. Buth. Techniques for Modelling Structured Operational and Denotational Semantics Definitions with Term Rewriting Systems. PhD thesis, Christian-Albrechts University, Kiel, 1994."},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"J. Camilleri and V. Zammit. Symbolic Animation as a Proof Tool. In HOL Theorem Proving System and its Applications. Springer-Verlag LNCS 859, 1994.","DOI":"10.1007\/3-540-58450-1_38"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"T. Despeyroux. Executable Specifications of Static Semantics. In International Symposium on Semantics of Data Types, 1984. Springer-Verlag LNCS 173.","DOI":"10.1007\/3-540-13346-1_11"},{"key":"35_CR8","unstructured":"J. Despeyroux. Proof of Translation in Natural Semantics. In Proceedings of the first ACM-IEEE Symp. on Logic In Computer Science, Cambridge, Ma, USA, June 1986, pages 193\u2013205, 1986. also available as a Research Report RR-514, Inria-Sophia-Antipolis, France, April 1986."},{"key":"35_CR9","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, Ch. Paulin, and B. Werner. The Coq Proof Assistant User's guide, Version 5.8. Technical Report 154, INRIA, Rocquencourt, May 1993."},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"J. Despeyroux and A. Hirschowitz. Higher-Order Abstract Syntax and Induction in Coq. In Proceedings of the 5 th Int. Conf. on Logic Programming and Automated Reasoning, July 1994.","DOI":"10.1007\/3-540-58216-9_36"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Howe. Generalization and Reuse of Tactic Proofs. In Proceedings of the 5 th Int. Conf. on Logic Programming and Automated Reasoning, July 1994.","DOI":"10.1007\/3-540-58216-9_25"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"J.V. Guttag and J.J.Horning, editors. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"35_CR13","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Technical Report 162, LFCS, University of Edinburgh, June 1991."},{"key":"35_CR14","volume-title":"Technical report","author":"I. Jacobs","year":"1992","unstructured":"I. Jacobs. The Centaur 1.2 Manual. Technical report, INRIA, Sophia-Antipolis, 1992."},{"key":"35_CR15","volume-title":"Proceedings of the Symp. on Theorical Aspects of Computer Science, Passau, Germany, 1987","author":"G. Kahn","year":"1987","unstructured":"G. Kahn. Natural Semantics. In Proceedings of the Symp. on Theorical Aspects of Computer Science, Passau, Germany, 1987. Also available as Research Report RR-601, INRIA, Sophia-Antipolis, February 1987."},{"key":"35_CR16","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1145\/151257.151260","volume":"number 2","author":"P. Klint","year":"1993","unstructured":"Paul Klint. A Meta-environment for Generating Programming Environments. In ACM Transaction on Software Engineering and Methodology, number 2 in 2, pages 176\u2013201, 1993.","journal-title":"ACM Transaction on Software Engineering and Methodology"},{"key":"35_CR17","unstructured":"M.J.C. Gordon and T.Melham. HOL: a Proof Generating System for Higher-order Logic. Cambridge University Press, 1992."},{"key":"35_CR18","unstructured":"F. Pfenning. Elf: A Language for Logic Definition and Verified Meta-Programming. In Proceedings of the 4 th International Symposium on Logic in Computer Science, June 1989."},{"key":"35_CR19","unstructured":"G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Aarhus, 1981."},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq: Rules and Properties. In Mark Bezem and Jan-Friso Groote, editors, Typed Lambda Calculi and Applications, pages 328\u2013345. Springer-Verlag, March 1993.","DOI":"10.1007\/BFb0037116"},{"key":"35_CR21","volume-title":"Implementing the Meta-Theory of Deductive Systems","author":"F. Pfenning","year":"1992","unstructured":"F. Pfenning and E. Rohwedder. Implementing the Meta-Theory of Deductive Systems. In D. Kapur, editor, Proceedings of the 11 th International Conference on Automated Deduction, Saratoga Springs, New York, June 1992."},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"R. Reetz and T. Kropf. Simplifying Deep Embedding: A Formalised Code Generator. In HOL Theorem Proving System and its Applications. Springer-Verlag LNCS 859, 1994.","DOI":"10.1007\/3-540-58450-1_55"},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"R. Roxas and M. Newey. Proof of Program Transformations. In HOL'91, HOL Theorem Proving System and its Applications, pages 223\u2013230. IEEE Computer Society Press, 1991.","DOI":"10.1109\/HOL.1991.596289"},{"key":"35_CR24","unstructured":"T. Reps and T. Teitelbaum. The Synthesizer Generator: a System for Constructing Language Based Editors. Springer Verlag, 1988. (third edition)."},{"key":"35_CR25","doi-asserted-by":"crossref","unstructured":"D. Terrasse. Encoding Natural Semantics in Coq. Submitted to AMAST'95. Also available by anonymous ftp to babar.inria.fr:pub\/croap\/terrasse:NSinCoq.dvi, 1994.","DOI":"10.1007\/3-540-60043-4_56"},{"key":"35_CR26","doi-asserted-by":"crossref","unstructured":"G. Winskel. The Formal Semantics of Programming Languages, an Introduction. Foundations of Computing. The MIT Press, 1993.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '95: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59293-8_218.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:27:03Z","timestamp":1619558823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59293-8_218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592938","9783540492337"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-59293-8_218","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}