{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:07:56Z","timestamp":1725494876874},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665885"},{"type":"electronic","value":"9783540481188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_10","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1128-1146","source":"Crossref","is-referenced-by-count":4,"title":["Interfacing program construction and verification"],"prefix":"10.1007","author":[{"given":"Richard","family":"Verhoeven","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Backhouse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"10_CR1","unstructured":"P. Anderson, M. Goldsmith, B. Scattergood, and T. Teitelbaum. An environment for intergrating formal methods tools. In Bertot [7]. See also: \n                    http:\/\/www.grammatech.com\/papers\/uitp.html\n                    \n                  ."},{"key":"10_CR2","unstructured":"Myla Archer, Constance Heitmeyer, and Steve Sims. TAME: A PVS interface to simplify proofs for automata models. In Backhouse [4], pages 147\u2013156. See also: \n                    http:\/\/www.win.tue.nl\/cs\/ipa\/uitp\/papers\/Archer.ps.gz\n                    \n                  ."},{"key":"10_CR3","unstructured":"R.C. Backhouse. Archive of the mathematics of program construction group. Available online at \n                    http:\/\/www.win.tue.nl\/cs\/wp\/papers\/\n                    \n                  , July 1998."},{"key":"10_CR4","unstructured":"R.C. Backhouse, editor. Workshop on User Interfaces for Theorem Provers, Computing Science Reports, July 1998. International Workshop, see also \n                    http:\/\/www.win.tue.nl\/cs\/ipa\/uitp\/proceedings.html\n                    \n                  ."},{"key":"10_CR5","first-page":"80","volume":"18","author":"R.C. Backhouse","year":"1997","unstructured":"R.C. Backhouse, R. Verhoeven, and O. Weber. Math\u2240pad: A system for on-line preparation of mathematical documents. Software-Concepts and Tools, 18: 80\u201389, 1997. See also: \n                    http:\/\/www.win.tue.nl\/cs\/wp\/mathspad\/\n                    \n                  .","journal-title":"Software-Concepts and Tools"},{"key":"10_CR6","unstructured":"Roland Backhouse and Richard Verhoeven. Math\u222bpad Ergonomic Document Preparation, version 0.60 edition, February 1996. Manual of the Math\u222bpad system. See also: \n                    http:\/\/www.win.tue.nl\/cs\/wp\/mathspad\/\n                    \n                  ."},{"key":"10_CR7","unstructured":"Yves Bertot, editor. Workshop on User Interfaces for Theorem Provers, September 1997. International Workshop, see also \n                    http:\/\/www-sop.inria.fr\/croap\/ events\/uitp97-papers.html\n                    \n                  ."},{"key":"10_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-60973-3_93","volume-title":"FME\u2019 96: Industrial Benefit and Advances in Formal Methods","author":"E. Boiten","year":"1996","unstructured":"Eerke Boiten, John Derrick, Howard Bowman, and Maarten Steen. Consistency and refinement for partial specification in z. In Marie-Claude Gaudel and James Woodcock, editors, FME\u2019 96: Industrial Benefit and Advances in Formal Methods, volume 1051 of LNCS, pages 287\u2013306. Springer, 1996."},{"key":"10_CR9","unstructured":"Bettina Buth. Operation Refinement Proofs for VDM-like Specifications. PhD thesis, Institute of Computer Science and Practical Mathematics of the Christian-Albrechts-University Kiel, February 1995. See also: \n                    http:\/\/www.informatik. uni-bremen.de\/~bb"},{"key":"10_CR10","unstructured":"Ingo Dahn. Using ILF as an interface to many theorem provers. In Backhouse [4], pages 75\u201386. See also: \n                    http:\/\/www.win.tue.nl\/cs\/ipa\/uitp\/papers\/Dahn.ps.gz\n                    \n                  ."},{"key":"10_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, Berlin, 1990."},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1093\/comjnl\/27.2.97","volume":"27","author":"D.E. Knuth","year":"1984","unstructured":"D.E. Knuth. Literate programming. Computer Journal, 27(2):97\u2013111, 1984.","journal-title":"Computer Journal"},{"key":"10_CR13","unstructured":"N.A. Merriam and M.D. Harrison. What is wrong with GUIs for theorem provers. In Bertot [7]. See also: \n                    http:\/\/www.cs.york.ac.uk\/~nam\/uitp97.ps.gz"},{"key":"10_CR14","volume-title":"The PVS Specification Language","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. See also: \n                    http:\/\/pvs.csl.sri.com\/\n                    \n                  ."},{"key":"10_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: a Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer, Berlin, 1994."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Darren Redfern. The Maple Handbook. Springer, 1996.","DOI":"10.1007\/978-1-4612-2344-3"},{"key":"10_CR17","unstructured":"John Rushby. What is pvs? Available online at \n                    http:\/\/pvs.csl.sri.com\/ whatispvs.html\n                    \n                  , November 1998. Contains a description of PVS."},{"key":"10_CR18","unstructured":"Frits D. Schalij. Tangram manual. Technical Report UR 008\/93, Philips Electronics N.V., 1996."},{"key":"10_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/BFb0028399","volume-title":"Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u2019 97","author":"M. Simons","year":"1997","unstructured":"Martin Simons. Proof presentation for Isabelle. In Elsa Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u2019 97, volume 1275 of Lecture Notes in Computer Science, pages 259\u2013274, Murray Hill, NJ, August 1997. Springer-Verlag."},{"key":"10_CR20","unstructured":"Bernard Sufrin and Richard Bornat. User interfaces for generic proof assistants part II: Displaying proofs. In Backhouse"},{"key":"10_CR21","unstructured":"Matteo Vaccari. Calculational Derivation of Circuits. PhD thesis, Dipartimento di Informatica, Universit\u00e0 degli Studi di Milano, May 1998. See also: \n                    http:\/\/ dotto.usr.dsi.unimi.it\/~matteo\/tesi.ps.gz"},{"key":"10_CR22","unstructured":"Stephen Wolfram. The Mathematica Book. Cambridge University Press, third edition, 1996."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T06:31:11Z","timestamp":1551508271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48118-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48118-4_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}