{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T14:59:45Z","timestamp":1709823585632},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1996,7,1]],"date-time":"1996-07-01T00:00:00Z","timestamp":836179200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1996,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We provide a mathematical specification of an extension of Warren's Abstract Machine (WAM) for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L.<\/jats:p>\n          <jats:p>In this paper, while leaving the details of the PAM's type constraint representation and solving facilities to a sequel to this work, we keep the notion of types and dynamic type constraints abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of B\u00f6rger's and Rosenzweig's formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND\/OR structure that are derived from B\u00f6rger's and Rosenzweig's corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.<\/jats:p>","DOI":"10.1007\/bf01213533","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T15:54:18Z","timestamp":1108742058000},"page":"428-462","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Specification and correctness proof of a WAM extension with abstract type constraints"],"prefix":"10.1145","volume":"8","author":[{"given":"Christoph","family":"Beierle","sequence":"first","affiliation":[{"name":"Fachbereich Informatik, LG Praktische Informatik VIII, FernUniversit\u00e4t Hagen, Bahnhofstr. 48, D-58084, Hagen, Germany"}]},{"given":"Egon","family":"B\u00f6rger","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, Italy"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/7160.001.0001"},{"key":"e_1_2_1_2_2_2","volume-title":"IWBS Report 200","author":"Beierle C.","year":"1991"},{"key":"e_1_2_1_2_3_2","volume-title":"Computer Science Logic \u2014 CSL'91. LNCS 626","author":"Beierle C.","year":"1992"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Beierle C. and B\u00f6rger E.: Refinement of a typed WAM extension by polymorphic order-sorted types. Formal Aspects of Computing 8(5) 1996 (to appear).","DOI":"10.1007\/BF01211908"},{"key":"e_1_2_1_2_5_2","volume-title":"Draft report of the logic programming language PROTOS-L. IWBS Report 175","author":"Beierle C.","year":"1991"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.363.0375"},{"key":"e_1_2_1_2_7_2","first-page":"377","volume-title":"Technology and Foundations \u2014Proceedings of the IFIP Congress 94, volume 1","author":"Beierle C.","year":"1994"},{"key":"e_1_2_1_2_8_2","first-page":"139","volume-title":"Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence","author":"Beierle C.","year":"1995"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90049-3"},{"key":"e_1_2_1_2_10_2","first-page":"272","volume-title":"Extending the Warren Abstract Machine to polymorphic order-sorted resolution","author":"Beierle C.","year":"1991"},{"key":"e_1_2_1_2_11_2","first-page":"36","volume-title":"LNCS 440","author":"Borger E.","year":"1990"},{"key":"e_1_2_1_2_12_2","first-page":"1","volume-title":"MFCS'90 \u2014Mathematical Foundations of Computer Science","author":"B\u00f6rger E.","year":"1990"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-54487-9_51","volume-title":"Computer Science Logic. LNCS 533","author":"B\u00f6rger E.","year":"1991"},{"key":"e_1_2_1_2_14_2","unstructured":"B\u00f6rger E. and Rosenzweig D.: The WAM \u2014 definition and compiler correctness. TR-14\/92 Dipartimento di Informatica Universit\u00e0 di Pisa 1992. (Revised version in: C. Beierle L. Pl\u00fcmer (Eds.) Logic Programming: Formal Methods and Practical Applications North-Holland 1995)."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-55460-2_4","volume-title":"Logic Programming. LNAI 592","author":"Borger E.","year":"1992"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-54487-9_52","volume-title":"Computer Science Logic. LNCS 533","author":"B\u00f6rger E.","year":"1991"},{"key":"e_1_2_1_2_17_2","unstructured":"B\u00f6rger E. and Salamone R.: CLAM specification for provably correct compilation of CLP(R) programs. In E. Borger editor Specification and Validation Methods pages 97\u2013130. Oxford University Press 1995."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/79204.79210"},{"key":"e_1_2_1_2_19_2","volume-title":"EATCS Monographs on Theoretical Computer Science","author":"Ehrig H.","year":"1989"},{"key":"e_1_2_1_2_20_2","unstructured":"Goguen J. A. and Meseguer J.: Eqlog: Equality types and generic modules for logic programming. In D. DeGroot and G. Lindstrom editors Logic Programming Functions Relations and Equations pages 295\u2013363. Prentice Hall 1986."},{"key":"e_1_2_1_2_21_2","unstructured":"Gurevich Y.: Logic and the challenge of computer science. In E. B\u00f6rger editor Trends in Theoretical Computer Science pages 1\u201357. Computer Science Press 1988."},{"key":"e_1_2_1_2_22_2","unstructured":"Gurevich Y.: Evolving algebras. A tutorial introduction. EATCS Bulletin 43 February 1991."},{"key":"e_1_2_1_2_23_2","unstructured":"Hanus M.: Horn Clause Specifications with Polymorphic Types. PhD thesis FB Informatik Universit\u00e4t Dortmund 1988."},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90107-S"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Jaffar J. and Lassez J.-L.: Constraint logic programming. In Proceedings of the 14th ACM Symposium on Principles of Programming Languages pages 111\u2013119. ACM January 1987.","DOI":"10.1145\/41625.41635"},{"key":"e_1_2_1_2_26_2","unstructured":"Jaffar J. Michaylov S. Stuckey P. and Yap R.: The CLP(\u211b) language and system. Technical Report RC 16292 IBM Research Devision 1990."},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(84)90017-1"},{"key":"e_1_2_1_2_28_2","first-page":"810","volume-title":"An overview of \u03bbProlog","author":"Nadathur G.","year":"1988"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90054-7"},{"key":"e_1_2_1_2_30_2","unstructured":"Smolka G.: TEL (Version 0.9) Report and User Manual. SEKI-Report SR 87-17 FB Informatik Universit\u00e4t Kaiserslautern 1988."},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Smolka G.: Logic Programming over Polymorphically Order-Sorted Types. PhD thesis FB Informatik Univ. Kaiserslautern 1989.","DOI":"10.1007\/3-540-50667-5_58"},{"key":"e_1_2_1_2_32_2","unstructured":"Warren D. H. D.: An Abstract PROLOG Instruction Set. Technical Report 309 SRI 1983."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01213533.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01213533\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01213533","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:26:55Z","timestamp":1641482815000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01213533"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,7]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1996,7]]}},"alternative-id":["10.1007\/BF01213533"],"URL":"https:\/\/doi.org\/10.1007\/bf01213533","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,7]]}}}