{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:21Z","timestamp":1767927861064,"version":"3.49.0"},"reference-count":23,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4521,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1016\/s0304-3975(99)00124-3","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T20:01:16Z","timestamp":1027627276000},"page":"151-185","source":"Crossref","is-referenced-by-count":42,"title":["Subtractive logic"],"prefix":"10.1016","volume":"254","author":[{"given":"Tristan","family":"Crolard","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(99)00124-3_BIB1","series-title":"Categories, Types and Structures","author":"Asperti","year":"1991"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB2","unstructured":"T. Crolard, Extension de l'isomorphisme de Curry-Howard au traitement des exceptions (application d'une \u00e9tude de la dualit\u00e9 en logique intuitionniste). Th\u00e9se de Doctorat. Universit\u00e9 Paris 7, 1996."},{"key":"10.1016\/S0304-3975(99)00124-3_BIB3","series-title":"Fondement de la topologie g\u00e9n\u00e9rale","author":"Cs\u00e1sz","year":"1960"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB4","series-title":"Foundations of Mathematical Logic","author":"Curry","year":"1963"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB5","doi-asserted-by":"crossref","unstructured":"D.J. Dougherty, R. Subrahmanyam, Equality between functionals in the presence of coproducts, in Proc. 10th Annual IEEE Symp. on Logic in Computer Science, 1995, pp. 282\u2013291.","DOI":"10.1109\/LICS.1995.523263"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB6","doi-asserted-by":"crossref","unstructured":"A.G. Dragalin, Mathematical intuitionism \u2014 introduction to proof theory, in: Translations of Mathematical Monographs, Vol. 67, American Matematical Society, Providence, RI, 1988.","DOI":"10.1090\/mmono\/067"},{"issue":"3","key":"10.1016\/S0304-3975(99)00124-3_BIB7","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","article-title":"Contraction-free sequent calculi for intuitionistic logic","volume":"57","author":"Dyckhoff","year":"1992","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB8","first-page":"224","volume":"Vol. 389","author":"Filinski","year":"1989"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB9","series-title":"Semantical Investigations in Heyting Intuitionistic Logic","author":"Gabbay","year":"1981"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB10","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","article-title":"A new constructive logic: classical logic","volume":"1","author":"Girard","year":"1991","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00124-3_BIB11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","article-title":"On the unity of logic","volume":"59","author":"Girard","year":"1993","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB12","volume":"Vol. 7","author":"Girard","year":"1988"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB13","first-page":"123","article-title":"Cartesian closed categories and lambda-calculus","volume":"Vol. 242","author":"Huet","year":"1986"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB14","volume":"Vol. 7","author":"Lambek","year":"1986"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB15","doi-asserted-by":"crossref","unstructured":"P.A. Mellies, Typed \u03bb-calculi with explicit substitutions may not terminate, in 2nd Internat. Conf. on Typed Lambda Calculi and Applications, LNCS, Edinburgh, UK, 1995, pp. 328\u2013334.","DOI":"10.1007\/BFb0014062"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB16","first-page":"41","article-title":"Model extension theorem and Graigs interpolation theorem for intermediate predicate logics","volume":"15","author":"Ono","year":"1983","journal-title":"Rep. Math. Logic"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB17","first-page":"190","volume":"Vol. 624","author":"Parigot","year":"1992"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB18","first-page":"263","volume":"Vol. 713","author":"Parigot","year":"1993"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB19","doi-asserted-by":"crossref","first-page":"219","DOI":"10.4064\/fm-83-3-219-249","article-title":"Semi-boolean algebras and their applications to intuitionistic logic with dual operations","volume":"83","author":"Rauszer","year":"1974","journal-title":"in Fund. Math."},{"key":"10.1016\/S0304-3975(99)00124-3_BIB20","unstructured":"C. Rauszer, An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, in Dissertationes Mathematicae, Vol. 167, Institut Math\u00e9matique de l'Acad\u00e9mie Polonaise des Sciences, 1980."},{"key":"10.1016\/S0304-3975(99)00124-3_BIB21","series-title":"Gentzen Collected Work","author":"Szabo","year":"1969"},{"key":"10.1016\/S0304-3975(99)00124-3_BIB22","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/BF02485724","article-title":"A categorical characterization of boolean algebras","volume":"4","author":"Szabo","year":"1974","journal-title":"Algebra Univ."},{"key":"10.1016\/S0304-3975(99)00124-3_BIB23","first-page":"225","volume":"Vol. 3","author":"van Dalen","year":"1986"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001243?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001243?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,15]],"date-time":"2020-01-15T22:22:11Z","timestamp":1579126931000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599001243"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["S0304397599001243"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00124-3","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}