{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:02Z","timestamp":1749124022624},"reference-count":27,"publisher":"Elsevier BV","issue":"2-3","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Future Generation Computer Systems"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1016\/0167-739x(96)88792-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T12:24:10Z","timestamp":1027599850000},"page":"123-137","source":"Crossref","is-referenced-by-count":2,"title":["Towards provably correct system synthesis and extension"],"prefix":"10.1016","volume":"12","author":[{"given":"Fausto","family":"Giunchiglia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Pecchiari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Armando","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0167-739X(96)88792-9_BIB1","article-title":"Backward logic tactics","author":"Armando","year":"1996"},{"key":"10.1016\/0167-739X(96)88792-9_BIB2","article-title":"Simple consequence relations","author":"Avron","year":"1987"},{"key":"10.1016\/0167-739X(96)88792-9_BIB3","unstructured":"M. Benerecetti and L. Spalazzi, Metafol: Program tactics and logic tactics plus reflection, in this issue."},{"key":"10.1016\/0167-739X(96)88792-9_BIB4","author":"Boyer","year":"1979"},{"key":"10.1016\/0167-739X(96)88792-9_BIB5","series-title":"The Correctness Problem in Computer Science","first-page":"103","article-title":"Metafunctions: proving them correct and using them efficiently as new proof procedures","author":"Boyer","year":"1981"},{"key":"10.1016\/0167-739X(96)88792-9_BIB6","author":"Boyer","year":"1988"},{"key":"10.1016\/0167-739X(96)88792-9_BIB7","series-title":"10th Int. Conf. on Automated Deduction","first-page":"1","article-title":"A theorem prover for a computational logic","author":"Boyer","year":"1990"},{"key":"10.1016\/0167-739X(96)88792-9_BIB8","series-title":"SAIL MEMO AIM-324","article-title":"Recursive programs as functions in a first order theory","author":"Cartwright","year":"1979"},{"key":"10.1016\/0167-739X(96)88792-9_BIB9","first-page":"88s","author":"Constable","year":"1986"},{"key":"10.1016\/0167-739X(96)88792-9_BIB10","series-title":"Proc. of VDM '91 (Formal Software Development Methods)","article-title":"Eves: An overview","volume":"Vol. 551","author":"Craigen","year":"1991"},{"issue":"1","key":"10.1016\/0167-739X(96)88792-9_BIB11","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF00881900","article-title":"Implementing tactics and tacticals in a higher-order logic programming language","volume":"11","author":"Felty","year":"1993","journal-title":"J. Automat. Reason."},{"key":"10.1016\/0167-739X(96)88792-9_BIB12","series-title":"Proc. 9th Conf. on Automated Deduction (CADE9)","first-page":"61","article-title":"Specifying theorem provers in a higher-order logic programming language","author":"Felty","year":"1988"},{"key":"10.1016\/0167-739X(96)88792-9_BIB13","article-title":"The GETFOL Manual \u2014 GETFOL version 1","author":"Giunchiglia","year":"1992"},{"key":"10.1016\/0167-739X(96)88792-9_BIB14","series-title":"Proc. META94","first-page":"425","article-title":"Introspective Metatheoretic Reasoning","volume":"Vol. 883","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0167-739X(96)88792-9_BIB15","article-title":"Reasoning theories: Towards an architecture for open mechanized reasoning systems","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0167-739X(96)88792-9_BIB16","unstructured":"F. Giunchiglia, P. Pecchiari and C. Talcott, An analysis of the interaction among the modules of the simplification process of the Boyer-Moore prover, in preparation."},{"issue":"2","key":"10.1016\/0167-739X(96)88792-9_BIB17","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0004-3702(95)00002-X","article-title":"A metatheory of a mechanized object theory","volume":"80","author":"Giunchiglia","year":"1996","journal-title":"J. Artificial Intelligence"},{"key":"10.1016\/0167-739X(96)88792-9_BIB18","series-title":"Proc. 5th Int. Conf. on Logic Programming and Automated Reasoning (LPAR'94)","article-title":"Program tactics and logic tactics","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0167-739X(96)88792-9_BIB19","series-title":"Research Topics in Functional Programming","first-page":"309","article-title":"Higher-order functions considered unnecessary for higher-order programming","author":"Goguen","year":"1990"},{"key":"10.1016\/0167-739X(96)88792-9_BIB20","article-title":"A Metalanguage for Interactive Proof in LCF","author":"Gordon","year":"1977"},{"key":"10.1016\/0167-739X(96)88792-9_BIB21","volume":"Vol. 78","author":"Gordon","year":"1979"},{"key":"10.1016\/0167-739X(96)88792-9_BIB22","series-title":"Proc. 9th Conf. on Automated Deduction (CADE9)","article-title":"Computational metatheory in Nuprl.","author":"Howe","year":"1988"},{"key":"10.1016\/0167-739X(96)88792-9_BIB23","article-title":"Design goals for ACL2","author":"Kaufmann","year":"1994"},{"key":"10.1016\/0167-739X(96)88792-9_BIB24","series-title":"Proc. Int. Lecture Series on \u201cFunctional Programming, Concurrency, Simulation and Automated Reasoning\u201d (FPCSAR)","article-title":"The eves system","author":"Kromodimoeljo","year":"1992"},{"key":"10.1016\/0167-739X(96)88792-9_BIB25","series-title":"Logic Colloquium '87","first-page":"275","article-title":"General logics","author":"Meseguer","year":"1989"},{"key":"10.1016\/0167-739X(96)88792-9_BIB26","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","article-title":"The foundation of a generic theorem prover","volume":"5","author":"Paulson","year":"1989","journal-title":"J. Automat. Reason"},{"key":"10.1016\/0167-739X(96)88792-9_BIB27","author":"Prawitz","year":"1965"}],"container-title":["Future Generation Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167739X96887929?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167739X96887929?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T17:59:15Z","timestamp":1556647155000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0167739X96887929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":27,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["0167739X96887929"],"URL":"https:\/\/doi.org\/10.1016\/0167-739x(96)88792-9","relation":{},"ISSN":["0167-739X"],"issn-type":[{"value":"0167-739X","type":"print"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}