{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:36:55Z","timestamp":1725457015321},"publisher-location":"Berlin\/Heidelberg","reference-count":13,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540557458"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0031928","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:11:55Z","timestamp":1134281515000},"page":"125-145","source":"Crossref","is-referenced-by-count":8,"title":["Formulas-as-types for a hierarchy of sublogics of intuitionistic propositional logic"],"prefix":"10.1007","author":[{"given":"Heinrich","family":"Wansing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P., The Lambda Calculus. Its Syntax and Semantics, North-Holland, Amsterdam, 1984."},{"key":"9_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-009-4540-1","volume-title":"Essays in Logical Semantics","author":"J.F.A.K. Benthem van","year":"1986","unstructured":"van Benthem, J.F.A.K., Essays in Logical Semantics, Reidel, Dordrecht, 1986."},{"key":"9_CR3","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/978-94-009-3673-7_11","volume-title":"Initiatives in Logic","author":"W. Buszkowski","year":"1987","unstructured":"Buszkowski, W., \u2018The Logic of Types', in: J. Srzednicki (ed), Initiatives in Logic, Martinus Nijhoff, Dordrecht, 1987, 180\u2013206."},{"key":"9_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-94-015-6878-4_4","volume-title":"Categorial Grammars and Natural Language Structures","author":"W. Buszkowski","year":"1988","unstructured":"Buszkowski, W., \u2018Generative Power of Categorial Grammars', in: R. Oehrle et.al. (eds.), Categorial Grammars and Natural Language Structures, Reidel, Dordrecht, 1988, 69\u201394."},{"key":"9_CR5","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00671566","volume":"47","author":"K. Do\u0161en","year":"1988","unstructured":"Do\u0161en, K., \u2018Sequent Systems and Groupoid Models, I', Studia Logica 47 (1988), 353\u2013389.","journal-title":"Studia Logica"},{"key":"9_CR6","unstructured":"Gabbay, D.M., de Queiroz, R.J.G.B., \u2018Extending the Curry-Howard Interpretation to Linear, Relevant and other Resource Logics', typescript, 1990."},{"key":"9_CR7","volume-title":"Introduction to Combinators and \u03bb-Calculus","author":"J.R. Hindley","year":"1986","unstructured":"Hindley, J.R., Seldin, J.P., Introduction to Combinators and \u03bb-Calculus, Cambridge UP, Cambridge, 1986."},{"key":"9_CR8","first-page":"479","volume-title":"To H.B.Curry. Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1969","unstructured":"Howard, W.A., \u2018The Formulae-as-Types-Notion of Construction', in: J.R. Hindley, J.P. Seldin (eds.), To H.B.Curry. Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London, 1980, 479\u2013490, (typescript, 1969)."},{"key":"9_CR9","volume-title":"Introduction to Higher Order Categorical Logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., Scott P., Introduction to Higher Order Categorical Logic, Cambridge UP, Cambridge, 1986."},{"key":"9_CR10","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0003-4843(77)80004-1","volume":"12","author":"G. Pottinger","year":"1977","unstructured":"Pottinger, G., \u2018Normalization as a Homomorphic Image of Cut-elimination', Annals of Mathematical Logic 12 (1977), 323\u2013357.","journal-title":"Annals of Mathematical Logic"},{"key":"9_CR11","unstructured":"Roorda, D., Resource Logics: Proof-theoretical Investigations, PhD Thesis, University of Amsterdam, 1991."},{"key":"9_CR12","first-page":"473","volume":"90","author":"R.C. Vrijer de","year":"1987","unstructured":"de Vrijer, R.C., \u2018Strong Normalization in N \u2014 HA\n\n                  p\n                  w\n                , Indagationes Mathematicae, Koninklijke Nederlandse Akademie van Wetenschappen, Proceedings, Series A, 90 (1987), 473\u2013478.","journal-title":"Koninklijke Nederlandse Akademie van Wetenschappen, Proceedings, Series A"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Wansing, H., \u2018Functional completeness for subsystems of intuitionistic propositional logic', Journal of Philosophical Logic, to appear.","DOI":"10.1007\/BF01049305"}],"container-title":["Lecture Notes in Computer Science","Nonclassical Logics and Information Processing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031928.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:05:23Z","timestamp":1607551523000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031928"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540557458"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0031928","relation":{},"subject":[]}}