{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T01:02:15Z","timestamp":1648515735833},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1989,9,1]],"date-time":"1989-09-01T00:00:00Z","timestamp":620611200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[1989,9]]},"DOI":"10.1007\/bf00370828","type":"journal-article","created":{"date-parts":[[2004,11,3]],"date-time":"2004-11-03T00:23:01Z","timestamp":1099441381000},"page":"319-360","source":"Crossref","is-referenced-by-count":3,"title":["Alpha-conversion, conditions on variables and categorical logic"],"prefix":"10.1007","volume":"48","author":[{"given":"Pierre-Louis","family":"Curien","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"N. De Bruijn, Lambda-calculus notation with nameless Dummies, a tool for automatic formula manipulation, Indag. Math. 34 (1972).","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"K. Bruce and G. Longo, A modest model of records, inheritance and bounded quantification, Proc. LICS 88, Edinburgh (1988).","DOI":"10.1109\/LICS.1988.5099"},{"key":"CR3","unstructured":"A. Burroni, Alg\ufffdbres graphiques, Cahiers de Topologie et G\ufffdom\ufffdtrie Diff\ufffdrentielle XXII-3 (1981)."},{"key":"CR4","unstructured":"CAML Primer and CAML Reference Manual, INRIA-ENS (1988)."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"L. Cardelli, The Amber machine, in Combinators and Functional Programming, LNCS 242 (1986).","DOI":"10.1007\/3-540-17184-3_39"},{"key":"CR6","unstructured":"J. Cartmell, Generalized algebraic theories and contextual categories, Thesis, Oxford (1978)."},{"key":"CR7","unstructured":"T. Coquand, Metamathematical investigations of a calculus of constructions, Technical Report, Cambridge University (1987)."},{"key":"CR8","unstructured":"T. Coquand, Sur l'analogie entre les propositions et les types, in cf. [5]."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"T. Coquand and T. Ehrhard, An equational presentation of higher order Logic, Proc. Second Summer Conference on Category Theory and Computer Science, Edinburgh LNCS283 (1987).","DOI":"10.1007\/3-540-18508-9_19"},{"key":"CR10","unstructured":"T. Coquand, C. Gunter and G. Winskel, Domain theoretic models of polymorphism, Technical Report 116, Cambridge University (1987)."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0167-6423(87)90020-7","volume":"8","author":"G. Cousineau","year":"1987","unstructured":"G. Cousineau, P.-L. Curien and M. Mauny, The categorical abstract machine, Science of Computer Programming 8 (1987), pp. 173?202.","journal-title":"Science of Computer Programming"},{"key":"CR12","unstructured":"G. Cousineau, P.-L. Curien, M. Mauny and A. Suarez, Combinateurs cat\ufffdgoriques et impl\ufffdmentation des langages fonctionnels, in cf. [5]."},{"issue":"1?3","key":"CR13","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/S0019-9958(86)80047-X","volume":"69","author":"P.-L. Curien","year":"1986","unstructured":"P.-L. Curien, Categorical combinators, Information and Control 69 (1?3) (1986), pp. 188?254.","journal-title":"Information and Control"},{"key":"CR14","unstructured":"P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman (1986)."},{"key":"CR15","unstructured":"P.-L. Curien and T. Ehrhard, Categories for dependent types, unpublished manuscript."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"T. Ehrhard, A categorical semantics of constructions, Proc. LICS 88, Edinburgh (1988).","DOI":"10.1109\/LICS.1988.5125"},{"key":"CR17","unstructured":"T. Ehrhard, Cat\ufffdgories et types variables, Thesis, in preparation."},{"key":"CR18","unstructured":"J.-Y. Girard, Interpr\ufffdtation fonctionnelle et elimination des coupures de l'arithm\ufffdtique d'ordre sup\ufffdrieur, Th\ufffdse de Doctorat d'Etat, Universit\ufffd Paris VII (1972)."},{"key":"CR19","unstructured":"J.-Y. Girard, Proof Theory and Logical Complexity, Bibliopolis (1987)."},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard, The system F of variable types, fifteen years later, Theoretical Computer Science (1986).","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"T. Hardin and A. Laville, Proof of termination of the rewriting system SUBST on CCL, Theoretical Computer Science 46 (1986).","DOI":"10.1016\/0304-3975(86)90035-6"},{"key":"CR22","unstructured":"T. Hardin, R\ufffdsultats de confluence pour les r\ufffdgles fortes de la logique combinatoire cat\ufffdgorique et liens avec les lambda-calculs, Th\ufffdse de Doctorat, Universit\ufffd Paris VII (Oct. 1987)."},{"key":"CR23","unstructured":"M. Hyland and A. Pitts, The theory of constructions: categorical semantics and topos-theoretic models, Proc. Conf. on Categories in Computer Science and Logic, to appear as Contemporary Mathematics volume, Boulder (1987)."},{"key":"CR24","unstructured":"J.-W. Klop and R. de Vrijer, Unique normal forms for lambda-calculus with surjective pairing, ITLI Technical Report, University of Amsterdam (1987)."},{"key":"CR25","unstructured":"Y. Lafont, Logiques, cat\ufffdgories et machines: implantation de langages de programmation guid\ufffde par la logique cat\ufffdgorique, Th\ufffdse de Doctorat, Universit\ufffd Paris VII (Jan. 1988)."},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"F. Lamarche, A simple model of the theory of constructions, in J. Gray and A. Scedrov (eds.), Categories in Computer Science and Logic, Contemporary Mathematics, to appear.","DOI":"10.1090\/conm\/092\/1003200"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"P. J. Landin, The mechanical evaluation of expressions, Computer Journal 6 (1964).","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"CR28","doi-asserted-by":"crossref","unstructured":"W. Lawvere, Adjointness in foundations, Dialectica 23 (3\/4) (1969).","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"W. Lawvere, Equality in hyperdoctrines and the comprehension schema as an adjoint functor, in Proc. New York Symposium on Applications of Categorical Logic, A. Heller (ed.), Amer. Math. Scoc. (1970).","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"CR30","unstructured":"G. Longo and E. Moggi, Constructive natural deduction and its modest interpretation, in Semantics of Natural and Programming Languages, J. Meseguer (ed.), M.I.T. Press, to appear (1988)."},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"S. Mac Lane, Categories for the Working Mathematician, Springer (1971).","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"CR32","unstructured":"P. Martin-L\ufffdf, Intuitionistic Type Theory, Bibliopolis (1984)."},{"key":"CR33","unstructured":"A. Obtu?owicz, Categorical and algebraic aspects of Martin-L\ufffdf type theory, this volume."},{"key":"CR34","unstructured":"A. Pitts, Polymorphism is set theoretic, constructively, cf. [9]."},{"key":"CR35","doi-asserted-by":"crossref","unstructured":"R. Seely, Hyperdoctrines, natural deduction and the Beck condition, Zeitschrift f\ufffdr Math. Logic und Grundlagen der Math. 29 (1983).","DOI":"10.1002\/malq.19830291005"},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"R. Seely, Locally cartesian closed categories and type theory, Mathematical Proceedings of Cambridge Philosophical Society 95 (1984).","DOI":"10.1017\/S0305004100061284"},{"key":"CR37","doi-asserted-by":"crossref","first-page":"969","DOI":"10.2307\/2273831","volume":"52","author":"R. Seely","year":"1987","unstructured":"R. Seely, Categorical semantics for higher order polymorphic lambda-calculus, Journal of Symbolic Logic 52 (1987), pp. 969?989.","journal-title":"Journal of Symbolic Logic"},{"key":"CR38","unstructured":"T. Streicher, Correctness and completeness of a semantics of the calculus of constructions with respect to interpretation in doctrines of constructions, Thesis, Universit\ufffdt Passau (1988)."},{"key":"CR39","unstructured":"P. Taylor, Recursive domains, indexed category theory and polymorphism, PhD Thesis, University of Cambridge (1986)."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00370828.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00370828\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00370828","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T18:28:04Z","timestamp":1585938484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00370828"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,9]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1989,9]]}},"alternative-id":["BF00370828"],"URL":"https:\/\/doi.org\/10.1007\/bf00370828","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,9]]}}}