{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:15:30Z","timestamp":1725455730703},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605898"},{"type":"electronic","value":"9783540478027"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015465","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:32:11Z","timestamp":1131863531000},"page":"239-254","source":"Crossref","is-referenced-by-count":4,"title":["Construction and deduction methods for the formal development of software"],"prefix":"10.1007","author":[{"given":"F. W.","family":"von Henke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Dold","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Schwier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Strecker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"S.F. Allen, R.L. Constable, D.J. Howe, and W.E. Aitken. The semantics of reflected proof. In Proc. 5th Annual IEEE Symposium on Logic in Computer Science, pages 95\u2013105. IEEE CS Press, 1990.","DOI":"10.1109\/LICS.1990.113737"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"L. Aiello and R.W. Weyhrauch. Using meta-theoretic reasoning to do algebra. In W. Bibel and R. Kowalksi, editors, 5th Conference on Automated Deduction, volume 87 of LNCS, pages 1\u201313. Springer, 1980.","DOI":"10.1007\/3-540-10009-1_1"},{"key":"13_CR3","unstructured":"R.S. Boyer and J.S. Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science, chapter 3. Academic Press, 1981."},{"issue":"1","key":"13_CR4","first-page":"10","volume":"7","author":"M. Broy","year":"1981","unstructured":"M. Broy and P. Pepper. Programming as a formal activity. IEEE Trans. on Software Engineering, 7(1):10\u201322, 1981.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"13_CR5","unstructured":"H.B. Curry and R. Feys. Combinatory Logic, volume 1. North Holland Publishing Company, 1958."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. Constructions: a Higher-Order Proof System for Mechanizing Mathematics. In B. Buchberger, editor, EUROCAL'85: European Conference on Computer Algebra, volume 203 of LNCS, pages 151\u2013184. Springer, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR8","unstructured":"CIP System Group. The Munich Project CIP \u2014 Volume II. volume 292 of LNCS. Springer, 1987."},{"key":"13_CR9","volume-title":"Implementing Mathematics with the NuPRL proof development system","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable et al. Implementing Mathematics with the NuPRL proof development system. Prentice Hall, Englewood Cliffs, NJ, 1986."},{"key":"13_CR10","unstructured":"A. Dold. Formalisierung schematischer Algorithmen. Ulmer Informatik-Berichte 94-10, Universit\u00e4t Ulm, January 1994."},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"K. G\u00f6del. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme. I. Monatsh. Math. Phys., 38:173\u2013198, 1931.","journal-title":"I. Monatsh. Math. Phys."},{"key":"13_CR12","unstructured":"F. Giunchiglia and A. Smaill. Reflection in Constructive and Non-Constructive Automated Reasoning. In Meta-Programming in Logic Programming, chapter 6, pages 123\u2013140. The MIT Press, 1989."},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang. Proving and applying program transformations expressed with second-order-patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"13_CR14","unstructured":"W.A. Howard. The Formulae-as-Types Notion of Construction. In J. Hindley and J. Seldin, editors, To H.B. Curry: Essays on Cornbinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"D.J. Howe. Computational metatheory in Nuprl. In Proc. 9th International Conference on Automated Deduction, volume 310 of LNCS, pages 238\u2013257. Springer, 1988.","DOI":"10.1007\/BFb0012835"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"R. Harper and R. Pollack. Type checking, universal polymorphism, and type ambiguity in the Calculus of Constructions. In TAPSOFT'89, volume II, volume 310 of LNCS, pages 240\u2013256. Springer, 1989.","DOI":"10.1007\/3-540-50940-2_39"},{"key":"13_CR17","unstructured":"T.B. Knoblock and R.L. Constable. Formalized metareasoning in type theory. In Proceedings of LICS, pages 237\u2013248. IEEE, 1986. Also available as technical report TR 86-742, Department of Computer Science, Cornell University."},{"key":"13_CR18","unstructured":"C. Kreitz. Metasynthesis \u2014 deriving programs that develop programs. Technical Report AIDA-93-03, Fachgebiet Intellektik, Technische Hochschule Darmstadt, 1993."},{"key":"13_CR19","unstructured":"Z. Luo. An Extended Calculus of Constructions. Technical Report CST-65-90, University of Edinburgh, July 1990."},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0890-5401(91)90062-7","volume":"90","author":"Z. Luo","year":"1991","unstructured":"Z. Luo. A Higher-Order Calculus and Theory Abstraction. Information and Computation, 90:107\u2013137, 1991.","journal-title":"Information and Computation"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Z. Luo. Program Specification and Data Refinement in Type Theory. In S. Abramsky and T.S.E. Maibaum, editors, TAPSOFT'91, volume I, volume 494 of LNCS, pages 143\u2013168. Springer, 1991.","DOI":"10.1007\/3-540-53982-4_9"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0890-5401(92)90031-A","volume":"99","author":"C. Ore","year":"1992","unstructured":"Ch.E. Ore. The extended calculus of constructions (ECC) with inductive types. Information and Computation, 99:231\u2013264, 1992.","journal-title":"Information and Computation"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th Intern. Conf. on Automated Deduction (CADE), volume 607 of LNAI, pages 748\u2013752. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"2","key":"13_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"H.A. Partsch. Specification and Transformation of Programs. Springer-Verlag, 1990.","DOI":"10.1007\/978-3-642-61512-2"},{"key":"13_CR26","unstructured":"H. Pfeifer. Eine reflexive Architektur zur Darstellung von Beweis-und SW-Entwicklungsschritten in Typtheorie. Master's thesis, Universit\u00e4t Ulm, 1995."},{"key":"13_CR27","unstructured":"H. Rue\u00df. Formal Meta-Programming in the Calculus of Constructions. PhD thesis, Universit\u00e4t Ulm, 1995."},{"key":"13_CR28","volume-title":"Technical Report KES.U.87.12","author":"D. R. Smith","year":"1987","unstructured":"D. R. Smith. Structure and design of global search algorithms. Technical Report KES.U.87.12, Kestrel Institute, Palo Alto, CA, 1987."},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. In Proc. TAPSOFT 89, volume 352 of LNCS, pages 375\u2013389. Springer, 1989.","DOI":"10.1007\/3-540-50940-2_48"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: model-theoretic foundations. In Proc. Intl. Colloq. on Automata, Languages and Programming, volume 623 of LNCS, pages 656\u2013671. Springer, 1992.","DOI":"10.1007\/3-540-55719-9_112"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"F. W. von Henke. An algebraic approach to data types, program verification, and program synthesis. In Mathematical Foundations of Computer Science, Proceedings, volume 45 of LNCS. Springer, 1976.","DOI":"10.1007\/3-540-07854-1_195"},{"key":"13_CR32","unstructured":"M. Wagner. Entwicklung und Implementierung eines Beweisers f\u00fcr konstruktive Logik. Master's thesis, Universit\u00e4t Ulm, 1995."},{"issue":"1","key":"13_CR33","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R. W. Weyhrauch","year":"1980","unstructured":"R. W. Weyhrauch. Prolegomena to a Theory of Mechanized Formal Reasoning. Artificial Intelligence, 13(1):133\u2013170, 1980.","journal-title":"Artificial Intelligence"},{"key":"13_CR34","unstructured":"M. Wirsing et al. A Method for the Development of Correct Software. 1995. In this volume."}],"container-title":["Lecture Notes in Computer Science","KORSO: Methods, Languages, and Tools for the Construction of Correct Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015465","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T20:47:35Z","timestamp":1586551655000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015465"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605898","9783540478027"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/bfb0015465","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}