{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:55:44Z","timestamp":1743072944631,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540875307"},{"type":"electronic","value":"9783540875314"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87531-4_14","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"169-183","source":"Crossref","is-referenced-by-count":2,"title":["A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Hermant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Lipton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Andrews, P.: Resolution in type theory. Journal of Symbolic Logic\u00a036(3) (1971)","DOI":"10.2307\/2269949"},{"key":"14_CR2","doi-asserted-by":"publisher","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. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR3","doi-asserted-by":"crossref","first-page":"644","DOI":"10.2307\/2272042","volume":"41","author":"H.C.M\u0303. Swart","year":"1976","unstructured":"de Swart, H.C.M\u0303.: Another intuitionistic completeness proof. Journal of Symbolic Logic\u00a041, 644\u2013662 (1976)","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"DeMarco, M., Lipton, J.: Completeness and cut elimination in the intuitionistic theory of types. Journal of Logic and Computation, 821\u2013854 (November 2005)","DOI":"10.1093\/logcom\/exi055"},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031, 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"14_CR6","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"14_CR7","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0064870","volume-title":"Logic Colloquium","author":"H. Friedman","year":"1975","unstructured":"Friedman, H.: Equality between functionals. In: Parikh, R. (ed.) Logic Colloquium. Lecture Notes in Mathematics, vol.\u00a0453, pp. 22\u201337. Springer, Heidelberg (1975)"},{"key":"14_CR8","volume-title":"Proceedings of the second Scandinavian proof theory symposium","author":"J.Y. Girard","year":"1971","unstructured":"Girard, J.Y.: Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse et son application \u00e0 l\u2019\u00e9limination de coupures dans l\u2019analyse et la th\u00e9orie des types. In: Fenstad, J.E. (ed.) Proceedings of the second Scandinavian proof theory symposium. North-Holland, Amsterdam (1971)"},{"key":"14_CR9","volume-title":"Proofs and Types","author":"J.Y. Girard","year":"1998","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1998)"},{"key":"14_CR10","first-page":"1","volume":"10","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Permutability of inferences in Gentzen\u2019s calculi LK and LJ. Memoirs of the American Mathematical Society\u00a010, 1\u201326, 27\u201368 (1952)","journal-title":"Memoirs of the American Mathematical Society"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"369","DOI":"10.2307\/2964012","volume":"23","author":"G. Kreisel","year":"1958","unstructured":"Kreisel, G.: A remark on free choice sequences and the topological completeness proofs. Journal of Symbolic Logic\u00a023, 369\u2013388 (1958)","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"139","DOI":"10.2307\/2964110","volume":"27","author":"G. Kreisel","year":"1962","unstructured":"Kreisel, G.: On weak completeness of intuitionistic predicate logic. Journal of Symbolic Logic\u00a027, 139\u2013158 (1962)","journal-title":"Journal of Symbolic Logic"},{"issue":"1-2","key":"14_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic\u00a051(1-2), 125\u2013157 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"14_CR14","volume-title":"Foundations for Programming Languages","author":"J. Mitchell","year":"1996","unstructured":"Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/S0304-3975(99)00058-4","volume":"227","author":"M. Okada","year":"1999","unstructured":"Okada, M.: Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. Theoretical Computer Science\u00a0227, 333\u2013396 (1999)","journal-title":"Theoretical Computer Science"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1016\/S0304-3975(02)00024-5","volume":"281","author":"M. Okada","year":"2002","unstructured":"Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science\u00a0281, 471\u2013498 (2002)","journal-title":"Theoretical Computer Science"},{"key":"14_CR17","volume-title":"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism","author":"G. Plotkin","year":"1980","unstructured":"Plotkin, G.: Lambda definability in the full type hierarchy. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York (1980)"},{"issue":"3","key":"14_CR18","doi-asserted-by":"publisher","first-page":"452","DOI":"10.2307\/2270331","volume":"33","author":"D. Prawitz","year":"1968","unstructured":"Prawitz, D.: Hauptsatz for higher order logic. The Journal of Symbolic Logic\u00a033(3), 452\u2013457 (1968)","journal-title":"The Journal of Symbolic Logic"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"305","DOI":"10.2307\/2963525","volume":"25","author":"K. Sch\u00fctte","year":"1960","unstructured":"Sch\u00fctte, K.: Syntactical and semantical properties of simple type theory. Journal of Symbolic Logic\u00a025, 305\u2013326 (1960)","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"980","DOI":"10.1090\/S0002-9904-1966-11611-7","volume":"72","author":"W. Tait","year":"1966","unstructured":"Tait, W.: A non-constructive proof of Gentzen\u2019s Hauptsatz for second-order predicate logic. Bulletin of the American Mathematical Society\u00a072, 980\u2013983 (1966)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Takahashi, M.-o.: A proof of cut-elimination in simple type theory. J. Math. Soc. Japan\u00a019(4) (1967)","DOI":"10.2969\/jmsj\/01940399"},{"key":"14_CR22","volume-title":"Constructivism in Mathematics: An Introduction","author":"A.S. Troelstra","year":"1988","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction, vol.\u00a02. Elsevier Science Publishers, Amsterdam (1988)"},{"key":"14_CR23","series-title":"Lecture Notes in Mathematics","first-page":"1","volume-title":"Lectures on Intuitionism","author":"D. van Dalen","year":"1973","unstructured":"van Dalen, D.: Lectures on Intuitionism. Lecture Notes in Mathematics, vol.\u00a0337, pp. 1\u201394. Springer, Heidelberg (1973)"},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"159","DOI":"10.2307\/2272955","volume":"41","author":"W. Veldman","year":"1976","unstructured":"Veldman, W.: An intuitionistic completeness theorem for intuitionistic predicate logic. Journal of Symbolic Logic\u00a041, 159\u2013166 (1976)","journal-title":"Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87531-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:12:38Z","timestamp":1715058758000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}