{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:58Z","timestamp":1725663718384},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540566106"},{"type":"electronic","value":"9783540475989"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56610-4_75","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:21:15Z","timestamp":1330255275000},"page":"343-355","source":"Crossref","is-referenced-by-count":3,"title":["Applications of type theory"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Mahr","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"24_CR1","unstructured":"Aczel, P.: Non-Wellfoundcd Sets, CSLI Lecture Notes 14, 1988"},{"key":"24_CR2","unstructured":"Barendregt, H.: Introduction to Generalized Type Systems, Tech. Report 90-8, Univ. of Nijmcgen, 1990."},{"key":"24_CR3","volume-title":"students thesis, Fachbereich 20","author":"S. Ballmann","year":"1991","unstructured":"Ballmann, S., Dunker, G.: Entwurf und Implementierung f\u00fcr den Kalk\u00fcl getypter Deklarationen, students thesis, Fachbereich 20, TU Berlin 1991"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bl\u00e4sius, K.H., Hcdtst\u00fcck, U., Rollinger, C.R. (eds): Sorts and Types in Artificial Intelligence, LNAI 418, Springer, 1990","DOI":"10.1007\/3-540-52337-6"},{"key":"24_CR5","unstructured":"Curry, H.B., Fcys, R.: Combinatory Logic, North Holland, 1958"},{"key":"24_CR6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple Theory of Types, J. Symb. Log. 5, 1940, 56\u201368","journal-title":"J. Symb. Log."},{"issue":"2\/3","key":"24_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"Th. Coquand","year":"1988","unstructured":"Coquand, Th., Huet, G.: The Calculus of Constructions, Information and Computation 76, 2\/3, 1988, 95\u2013120","journal-title":"Information and Computation"},{"key":"24_CR8","unstructured":"Coquand, Th.: Une th\u00e9orie des constructions, Th\u00e8se, Universit\u00e9 Paris VII, 1985"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1, Springer-Verlag, 1985","DOI":"10.1007\/978-3-642-69962-7"},{"key":"24_CR10","unstructured":"Fraenkel, A.A., Bar-Hillel, Y., Levy, A.: Foundations of Set Theory, North-Holland, 1984"},{"key":"24_CR11","unstructured":"Gentzen, G.: The collected Papers of Gerhard Gcntzcn. ed E. Szabo, North Holland, 1969"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse et son application \u00e0 r \u00e9limination des conpures dans l'analyse et dans le th\u00e9orie des types, Proc. of the Zud Scandinavian Logic Symposium (ed. LE. Fenstad), North Holland, 1971, 63\u201392","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"24_CR13","unstructured":"Herbrand, J.: Investigations in Proof Theory (1930) in: Logical Writings, ed. W.D. Goldfarb, Reidel, 1971"},{"key":"24_CR14","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1002\/mana.19630270108","volume":"27","author":"P. J. Higgins","year":"1963","unstructured":"Higgins, P.J.: Algebra with a scheme of operators, Mathematische Nachrichten, 27, 1963, 115\u2013132","journal-title":"Mathematische Nachrichten"},{"key":"24_CR15","unstructured":"Howard, W.A.: The formulae-as-Types notion of construction, in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, ed. J.P. Seklin and J.R. Hindley, Academic Press, 1980, 479\u2013490"},{"key":"24_CR16","unstructured":"Luo, Z.: An Extended Calculus of Constructions, Dept. of Comp. Science, Univ. of Edinburgh, 1990"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. R. Meyer","year":"1982","unstructured":"Meyer, A.R.: What is a model of Lambda Calculus? in: Information and Control 52, 1982, 87\u2013122","journal-title":"Information and Control"},{"key":"24_CR18","first-page":"384","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A Theory of Type Polymorphism in Programming, J.C.S.S. 17, 1978, 384\u2013375","journal-title":"J.C.S.S."},{"key":"24_CR19","unstructured":"Martin-L\u00f6f, P.: A Theory or Types, Report 71-3, Dept. of Math., Univ. of Stockholm, 1971"},{"key":"24_CR20","first-page":"153","volume":"6","author":"P. Martin-L\u00f6f","year":"1980","unstructured":"Martin-L\u00f6f, P.: Constructive Mathematics and Computer Programming, Logic, Methodology and Philosophy of Science 6, 1980, 153\u2013175","journal-title":"Logic, Methodology and Philosophy of Science"},{"key":"24_CR21","unstructured":"Martin-L\u00f6f, P.: Intuitionislic Type Theory, Bibliopolis, 1984"},{"key":"24_CR22","unstructured":"Mahr, B., Str\u00e4ter, W., Um bach, C.: Fundamentals of a Theory of Types and Declarations, KIT-Rcport 82, TU Berlin, Fachbereich 20, 1990"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, B.: Programming in Constructive Set Theory: Some Examples. Proc. ACM Conf. of Funct. Prog. Lang. and Comp. Arch., ACM, 1981, 141\u2013154","DOI":"10.1145\/800223.806773"},{"key":"24_CR24","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6fs' Type Theory, Clarendon Press, 1990"},{"key":"24_CR25","unstructured":"Pooyan, L.: \u03b5-structures as Semantic Models of the \u03bb-calculus, Diploma Thesis, Fachbereich Informatik, TU Berlin, 1992"},{"key":"24_CR26","unstructured":"Quinc, W.O.: Mengenlehre und ihre Logik, Vieweg, 1973, First published in 1963"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Towards a Theory of Type Structure, LNCS 19, Springer-Verlag, 1974,408\u2013425","DOI":"10.1007\/3-540-06859-7_148"},{"key":"24_CR28","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B. Russell","year":"1908","unstructured":"Russell, B.: Mathematical Logic as based on the theory of types, Am. J. Math. 30, 1908, 222\u2013262","journal-title":"Am. J. Math."},{"key":"24_CR29","unstructured":"Str\u00e4ter, W.: \u03b5T Eine Logik erster Stufe mit Selbstreferenz und totalem Wahrheilspr\u00e4dikal, KIT-Rcporl 98, TU Berlin, Fachbereich 20, 1992"},{"key":"24_CR30","unstructured":"Str\u00e4ter, W.: Internal notes on non wcllfounded sets, Fachbereich 20, TU Berlin, 1992"},{"key":"24_CR31","unstructured":"Thompson, S.: Type Theory and Functional Programming, Addison-Wesley, 1991"},{"key":"24_CR32","unstructured":"Umbach, C.: A standard discipline in the calculus of declarations. Internal notes, Fachbereich 20, TU Berlin, 1991"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT'93: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56610-4_75.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:05:03Z","timestamp":1605647103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56610-4_75"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540566106","9783540475989"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-56610-4_75","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}