{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:31Z","timestamp":1761611071467},"reference-count":35,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1992,10,1]],"date-time":"1992-10-01T00:00:00Z","timestamp":717897600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7594,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1992,10]]},"DOI":"10.1016\/0304-3975(92)90169-g","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"129-159","source":"Crossref","is-referenced-by-count":12,"title":["A theory for program and data type specification"],"prefix":"10.1016","volume":"104","author":[{"given":"Carolyn","family":"Talcott","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(92)90169-G_BIB1","series-title":"Structure and Interpretation of Computer Programs","author":"Abelson","year":"1985"},{"key":"10.1016\/0304-3975(92)90169-G_BIB2","series-title":"Foundations of Constructive Mathematics","author":"Beeson","year":"1985"},{"key":"10.1016\/0304-3975(92)90169-G_BIB3","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF00625280","article-title":"Partial abstract types","volume":"18","author":"Broy","year":"1982","journal-title":"Acta Inform."},{"issue":"1","key":"10.1016\/0304-3975(92)90169-G_BIB4","doi-asserted-by":"crossref","DOI":"10.1145\/9758.10501","article-title":"On the algebraic definition of programming languages","volume":"9","author":"Broy","year":"1987","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0304-3975(92)90169-G_BIB5","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1147\/rd.191.0012","article-title":"Stream processing functions","volume":"19","author":"Burge","year":"1975","journal-title":"IBM J. Res. Develop."},{"key":"10.1016\/0304-3975(92)90169-G_BIB6","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1145\/366663.366704","article-title":"Design of a separable transition-diagram compiler","volume":"6","author":"Conway","year":"1963","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(92)90169-G_BIB7","series-title":"Automata, Languages and Programming, 12th Colloq.","first-page":"120","article-title":"A completeness theorem for recursively defined types","volume":"Vol. 194","author":"Coppo","year":"1985"},{"key":"10.1016\/0304-3975(92)90169-G_BIB8","series-title":"Algebra and Logic","first-page":"87","article-title":"A language and axioms for explicit mathematics","volume":"Vol. 450","author":"Feferman","year":"1975"},{"key":"10.1016\/0304-3975(92)90169-G_BIB9","series-title":"Logic Colloquium \u201978","first-page":"159","article-title":"Constructive theories of functions and classes","author":"Feferman","year":"1979"},{"key":"10.1016\/0304-3975(92)90169-G_BIB10","series-title":"Logic Colloquium \u201980","first-page":"95","article-title":"Inductively presented systems and the formalization of meta-mathematics","author":"Feferman","year":"1982"},{"key":"10.1016\/0304-3975(92)90169-G_BIB11","first-page":"95","article-title":"A theory of variable types","volume":"19","author":"Feferman","year":"1985","journal-title":"Rev. Colombiana Mat."},{"key":"10.1016\/0304-3975(92)90169-G_BIB12","article-title":"Logics for termination and correctness of functional programs, I","author":"Feferman","year":"1989","journal-title":"Logic from Computer Science, MSRI, Berkeley, CA"},{"key":"10.1016\/0304-3975(92)90169-G_BIB13","series-title":"Logic and Computation","first-page":"101","article-title":"Polymorphic typed lambda-calculi in a type-free axiomatic framework","volume":"Vol. 106","author":"Feferman","year":"1990"},{"key":"10.1016\/0304-3975(92)90169-G_BIB14","article-title":"Logics for termination and correctness of functional programs, II","author":"Feferman","year":"1990","journal-title":"Leeds Proof Theory"},{"key":"10.1016\/0304-3975(92)90169-G_BIB15","series-title":"PhD thesis","article-title":"The calculi of lambda-v-cs conversion: A syntactic theory of control and state in imperative higher-order programming languages","author":"Felleisen","year":"1987"},{"key":"10.1016\/0304-3975(92)90169-G_BIB16","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","article-title":"A syntactic theory of sequential control","volume":"52","author":"Felleisen","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(92)90169-G_BIB17","series-title":"Technical Report COMP TR89-100","article-title":"The revised report on the syntactic theories of sequential control and state","author":"Felleisen","year":"1989"},{"key":"10.1016\/0304-3975(92)90169-G_BIB18","series-title":"CTRS'90","article-title":"A simplifier for untyped lambda expressions","volume":"Vol. 516","author":"Galbiati","year":"1990"},{"key":"10.1016\/0304-3975(92)90169-G_BIB19","first-page":"47","article-title":"Formulae as types notion of control","author":"Griffin","year":"1990","journal-title":"17th Ann. ACM Symp. on Principles of Programmings Languages"},{"key":"10.1016\/0304-3975(92)90169-G_BIB20","series-title":"PX: A Computational Logic","author":"Hayashi","year":"1988"},{"key":"10.1016\/0304-3975(92)90169-G_BIB21_1","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/363744.363749","article-title":"A correspondence between Algol 60 and Church's lambda notation","volume":"8","author":"Landin","year":"1965","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(92)90169-G_BIB21_2","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1145\/363791.363804","article-title":"A correspondence between Algol 60 and Church's lambda notation","volume":"8","author":"Landin","year":"1965","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(92)90169-G_BIB22","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/365230.365257","article-title":"The next 700 programming languages","volume":"9","author":"Landin","year":"1966","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(92)90169-G_BIB23","series-title":"Mathematical Theory of Computation","author":"Manna","year":"1974"},{"key":"10.1016\/0304-3975(92)90169-G_BIB24","series-title":"4th Ann. Symp. on Logic in Computer Science","first-page":"14","article-title":"Computational lambda-calculus and monads","author":"Moggi","year":"1989"},{"key":"10.1016\/0304-3975(92)90169-G_BIB25","article-title":"An evaluation semantics for classical proofs, manuscript","author":"Murthy","year":"1991","journal-title":"Procs. LICS '91"},{"key":"10.1016\/0304-3975(92)90169-G_BIB26","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value an the lambda-v-calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoret. Comput. Sci."},{"issue":"12","key":"10.1016\/0304-3975(92)90169-G_BIB27","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/15042.15043","article-title":"The revised3 report on the algorithmic language scheme","volume":"21","year":"1986","journal-title":"SIGPLAN Notices"},{"key":"10.1016\/0304-3975(92)90169-G_BIB28","first-page":"717","article-title":"Definitional interpreters for higher-order programming languages","author":"Reynolds","year":"1972","journal-title":"Proc. ACM National Convention"},{"key":"10.1016\/0304-3975(92)90169-G_BIB29","series-title":"Technical Report Technical Monograph PRG-6","article-title":"Towards a mathematical semantics for computer languages","author":"Scott","year":"1971"},{"key":"10.1016\/0304-3975(92)90169-G_BIB30","series-title":"Technical Report TR 88-938","article-title":"Partial objects in type theory","author":"Smith","year":"1988"},{"key":"10.1016\/0304-3975(92)90169-G_BIB31","series-title":"Common Lisp: The Language","author":"Steele","year":"1990"},{"key":"10.1016\/0304-3975(92)90169-G_BIB32","series-title":"Technical Report Technical Report 349","article-title":"Scheme, an interpreter for extended lambda calculus","author":"Steele","year":"1975"},{"key":"10.1016\/0304-3975(92)90169-G_BIB33","series-title":"PhD thesis","article-title":"The essence of rum: A theory of the intensional and extensional aspects of Lisp-type computation","author":"Talcott","year":"1985"},{"key":"10.1016\/0304-3975(92)90169-G_BIB34","series-title":"Technical Report STANCS-89-1288","article-title":"Programming and proving function and control abstractions","author":"Talcott","year":"1989"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759290169G?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759290169G?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T04:20:21Z","timestamp":1555129221000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759290169G"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,10]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,10]]}},"alternative-id":["030439759290169G"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(92)90169-g","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1992,10]]}}}