{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:51:15Z","timestamp":1725663075377},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540185086"},{"type":"electronic","value":"9783540480068"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/3-540-18508-9_19","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:36:23Z","timestamp":1330198583000},"page":"40-56","source":"Crossref","is-referenced-by-count":7,"title":["An equational presentation of higher order logic"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Ehrhard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"3_CR1","first-page":"72","volume":"62","author":"G. Berry","year":"1978","unstructured":"Berry, G. \u201cStable models of the typed \u03bb-calculi\u201d ICALP, Springer-Verlag, LNCS 62, 1978 pp. 72\u201389","journal-title":"ICALP, Springer-Verlag, LNCS"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen and A. Meyer. \u201cLambda Calculus with Constrained Types\u201d Abstract (1985)","DOI":"10.1007\/3-540-15648-8_3"},{"key":"3_CR3","unstructured":"A. Burroni. \u201cAlg\u00e8bres graphiques\u201d Cahiers de Topologie et Geometrie Differentielle Volume XXII-3 1981"},{"key":"3_CR4","first-page":"50","volume":"201","author":"G. Cousineau","year":"1985","unstructured":"G. Cousineau, P.L. Curien and M. Mauny. \u201cThe Categorical Abstract Machine.\u201d In Functional Programming Languages and Computer Architecture, Ed. J. P. Jouannaud, Springer-Verlag LNCS 201 (1985) 50\u201364.","journal-title":"LNCS"},{"key":"3_CR5","unstructured":"T. Coquand, C. Gunter, G. Winskel. \u201cPolymorphism and domain equations\u201d Technical report Cambridge no 107."},{"key":"3_CR6","unstructured":"P. L. Curien. \u201cCategorical Combinators, Sequential Algorithms and Functional Programming.\u201d Research Notes in Theoretical computer Science, Pitman (1986)."},{"key":"3_CR7","unstructured":"P. L. Curien \u201cCategorical combinators for (existential) quantification\u201d unpublished notes."},{"issue":"5","key":"3_CR8","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn. \u201cLambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.\u201d Indag. Math. 34,5 (1972), 381\u2013392.","journal-title":"Indag. Math."},{"issue":"1","key":"3_CR9","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. \u201cA formulation of the simple theory of types.\u201d Journal of Symbolic Logic 5,1 (1940) 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"3_CR10","unstructured":"P. Gabriel and F. Ulmer. \u201cLokal Pr\u00e4sentierbare Kategorien\u201d Lecture Notes in Mathematics, Vol. 221 (Springer, Berlin)."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"R.O. Gandy. \u201cOn the axiom of extensionality-Part I.\u201d J.S.L. 21 (1956).","DOI":"10.2307\/2268484"},{"key":"3_CR12","unstructured":"J.Y. Girard. \u201cInterpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure.\u201d Th\u00e8se d'Etat, Universit\u00e9 Paris VII (1972)."},{"key":"3_CR13","unstructured":"J.Y. Girard. \u201cThe system F of variable types, fifteen years later\u201d in TCS 86."},{"key":"3_CR14","unstructured":"C. Gunter. \u201cProfinite Solutions for Recursive Domain Equations\u201d PhD thesis, CMU, (1985)."},{"key":"3_CR15","unstructured":"W. A. Howard. \u201cThe formul\u00e6-as-types notion of construction.\u201d Unpublished manuscript (1969). Reprinted in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds J. P. Seldin and J. R. Hindley, Academic Press (1980)."},{"key":"3_CR16","unstructured":"G. Huet. \u201cCartesian closed categories and Lambda-Calculus\u201d in Combinators and functional programming languages Eds P.L. Curien, G. Cousineau et B. Robinet. LNCS 242"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland, P.T. Johnstone, A.M. Pitts. \u201cTripos theory.\u201d Math. Proc. Camb. Phil. Soc. 88 (1980).","DOI":"10.1017\/S0305004100057534"},{"key":"3_CR18","unstructured":"J. Lambek and P. J. Scott. \u201cIntroduction to higher order categorical logic\u201d Cambridge studies in advanced mathematics, Cambridge University Press, 1986."},{"key":"3_CR19","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"Lawvere","year":"1969","unstructured":"Lawvere. \u201cAdjointness in foundations\u201d Dialectica 23 (1969) 281\u2013296.","journal-title":"Dialectica"},{"key":"3_CR20","unstructured":"P. Martin-L\u00f6f. \u201cIntuitionistic Type Theory.\u201d Bibliopolis (1982)."},{"key":"3_CR21","unstructured":"N. McCracken. \u201cAn investigation of a programming language with a polymorphic type structure.\u201d Ph.D. Dissertation, Syracuse University (1979)."},{"key":"3_CR22","unstructured":"R. Par\u00e9, D. Schumacher. \u201cIndexed Categories and Their Applications.\u201d Springer-Verlag, Lecture Notes in Mathematics, 661."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"M.B. Plotkin and G.D. Smyth. \u201cThe category-theoretic solution of recursive domain equations\u201d SIAM J. COMPUT. Vol. 11, No 4, November 1982","DOI":"10.1137\/0211062"},{"key":"3_CR24","unstructured":"D. Scott. \u201cRelating Theories of the Lambda-Calculus.\u201d in To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Eds. J. P. Seldin and J. R. Hindley, Academic Press (1980)."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"R.A.G. Seely. \u201cHyperdoctrines, natural deduction and the Beck condition\u201d Zeitschrift f\u00fcr Mat. Logik und Grundlagen d. Math. 29 505\u2013542.","DOI":"10.1002\/malq.19830291005"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"R.A.G Seely. \u201cLocally Cartesian Closed Categories and Type Theory\u201d Math. Proc. Camb. Phil. Soc. 95, 1984.","DOI":"10.1017\/S0305004100061284"},{"key":"3_CR27","unstructured":"R.A.G. Seely. \u201cCategorical Semantics for Higher Order Polymorphic Lambda Calculus\u201d Draft."},{"key":"3_CR28","unstructured":"J.E. Stoy. \u201cDenotational Semantics: the Scott-Strache Approach to the Programming Language Theory\u201d The M.I.T. Press, Cambridge, Massachussetts, and London, England."},{"key":"3_CR29","unstructured":"G. Takeuti. \u201cProof theory.\u201d Studies in Logic 81 Amsterdam (1975)."}],"container-title":["Lecture Notes in Computer Science","Category Theory and Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-18508-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:59Z","timestamp":1605644099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-18508-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540185086","9783540480068"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-18508-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1987]]}}}