{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:30Z","timestamp":1725663450195},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540549673"},{"type":"electronic","value":"9783540466123"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54967-6_61","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:22:24Z","timestamp":1330194144000},"page":"57-70","source":"Crossref","is-referenced-by-count":0,"title":["On the operational interpretation of complex types"],"prefix":"10.1007","author":[{"given":"Qing-Ping","family":"Tan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huo-Wang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","unstructured":"T.Coquand & C.Paulin:: \u201dInductively Defined Types\u201d, Proc. of International Conference on Computer Logic, L.N.C.S. 417,1988."},{"key":"5_CR2","unstructured":"A.Felry & A. Miller: \u201d Specifying Theorem Provers in a Higher-Order Logic Programming Language\u201d, Proc. of CADE'88, L.N.C.S. 310,1988."},{"key":"5_CR3","unstructured":"R.Harper & R.Honsell & G.Plotkin: \u201d A Framework for Defining Logics\u201d, Proc. of LICS'87, 1987."},{"key":"5_CR4","unstructured":"Zhaohui Luo: \u201d An Extended Calculus of Constructions\u201d, Ph.D. Thesis, Univ. of Edinburgh, 1990."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"L.Paulson:\u201d The Foundations of a Generic Theorem Prover\u201d, Journal of Automated Reasoning, Vol. 5, 1989.","DOI":"10.1007\/BF00248324"},{"key":"5_CR6","unstructured":"K.Petersson: \u201d A Set Constructor for Inductive Sets in Martin-Lof Type Theory\u201d, Proc. of Category Method in Computer Science, L.N.C.S. 389,1898."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"F.Pfenning: \u201d Elf: A Language for Logic Definition and Verified Metaprogramming\u201d, Proc. of LICS'89, 1989.","DOI":"10.1109\/LICS.1989.39186"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54967-6_61.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:56:59Z","timestamp":1605628619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54967-6_61"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540549673","9783540466123"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-54967-6_61","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}