{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T03:40:06Z","timestamp":1735530006078,"version":"3.32.0"},"reference-count":7,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1993,8,1]],"date-time":"1993-08-01T00:00:00Z","timestamp":744163200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,8]]},"DOI":"10.1007\/bf01383982","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:08:55Z","timestamp":1112407735000},"page":"7-24","source":"Crossref","is-referenced-by-count":4,"title":["The HOL logic extended with quantification over type variables"],"prefix":"10.1007","volume":"3","author":[{"given":"Thomas F.","family":"Melham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"M.J.C. Gordon and T.F. Melham (eds).Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types.The Journal of Symbolic Logic, 5:56?68 (1940).","journal-title":"The Journal of Symbolic Logic"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, A.J. Milner, and C.P. Wadsworth.Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, vol. 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"J.-Y. Girard. The system F of variable types, fifteen years later.Theoretical Computer Science, 45: 159?192 (1986).","journal-title":"Theoretical Computer Science"},{"key":"CR5","unstructured":"P.B. Andrews.A Transfinite Type Theory with Type Variables, Studies in Logic and the Foundations of Mathematics series, North-Holland, 1965."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"T. Melham. A package for inductive relation definitions in HOL.Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley (eds) IEEE Computer Society Press, 1992, 350?357.","DOI":"10.1109\/HOL.1991.596299"},{"key":"CR7","unstructured":"K. Slind. An Implementation of Higher Order Logic. Research Report 91\/419\/03, Department of Computer Science, University of Calgary, 1991."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383982.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383982\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383982","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T02:34:44Z","timestamp":1735526084000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383982"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,8]]},"references-count":7,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1993,8]]}},"alternative-id":["BF01383982"],"URL":"https:\/\/doi.org\/10.1007\/bf01383982","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1993,8]]}}}