{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T00:40:09Z","timestamp":1738975209074,"version":"3.37.0"},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5847,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1993,3]]},"abstract":"<jats:p>We present an algebraic approach to the syntax and semantics of Martin-L\u00f6f type theory and the calculus of constructions developed by T. Coquand and G. Huet. In our approach, models of this theory and this calculus are treated as three-sorted partial algebras, called ITS\u03a0-structures, described by essentially algebraic theories. We give a proof that derived statements of Martin-L\u00f6f type theory hold in appropriate ITS\u03a0-structures. In this proof, a formal translation from the language of terms and types into the language of terms of an appropriate essentially algebraic theory of ITS\u03a0-structures is used. A straightforward set-theoretic construction of ITS\u03a0-structures that are models of Martin-L\u00f6f type theory is demonstrated. We present a construction of a recursive ITS\u03a0-structure<jats:italic>(i.e<\/jats:italic>. its partial and total operations are recursive functions over some alphabet) that is a model of the calculus of constructions and demonstrates the decidability of this calculus.<\/jats:p>","DOI":"10.1017\/s0960129500000128","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:01:47Z","timestamp":1236157307000},"page":"63-92","source":"Crossref","is-referenced-by-count":0,"title":["Algebra of constructions II: an algebraic approach to Martin-L\u00f6f type theory and the calculus of constructions"],"prefix":"10.1017","volume":"3","author":[{"given":"Adam","family":"Obtu\u0142owicz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000128_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90018-6"},{"key":"S0960129500000128_ref008","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","article-title":"Modular proof of strong normalization for the calculus of constructions","volume":"1","author":"Geuvers","year":"1991","journal-title":"Journal of Functional Programming"},{"volume-title":"Formal Structures for Computation and Deduction","year":"1986","author":"Huet","key":"S0960129500000128_ref012"},{"key":"S0960129500000128_ref018","unstructured":"Streicher T. (1988) Correctness and Completeness of Categorical Semantics of the Calculus of Constructions, Ph. D. Thesis, Passau Universit\u00e4t."},{"key":"S0960129500000128_ref009","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"S0960129500000128_ref001","doi-asserted-by":"crossref","DOI":"10.1515\/9783112720875","volume-title":"A Model Theoretic Oriented Approach to Partial Algebras","author":"Burmeister","year":"1986"},{"key":"S0960129500000128_ref015","unstructured":"Obtu\u0142owicz A. (1991) Remarks on term rewriting systems extracted from some theories of certain categories, talk given at LMS Durham Symposium on Applications of Categories in Computer Science, July 20\u201330 1991."},{"key":"S0960129500000128_ref010","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-77487-9","volume-title":"Universal Algebra","author":"Gr\u00e4tzer","year":"1979"},{"key":"S0960129500000128_ref016","unstructured":"Ritter E. (1990) Categorical Combinators for the Calculus of Constructions, Thesis, University of Cambridge."},{"key":"S0960129500000128_ref003","first-page":"795","article-title":"Near-equational and Equational System of Logic for Partial Functions","volume":"54","author":"Craig","year":"1989","journal-title":"J. S. L"},{"key":"S0960129500000128_ref006","volume":"VII","author":"Ehrhard","year":"1988","journal-title":"Une S\u00e9mantique Cat\u00e9gorique des Types D\u00e9pendants Application au Calculus des Constructions"},{"volume-title":"Introduction to Combinators and \u03bb-calculus","year":"1986","author":"Hindley","key":"S0960129500000128_ref011"},{"key":"S0960129500000128_ref007","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700044828"},{"key":"S0960129500000128_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"volume-title":"Categorical Combinators, Sequential Algorithms and Functional Programming","year":"1986","author":"Curien","key":"S0960129500000128_ref004"},{"key":"S0960129500000128_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0960129500000128_ref013","article-title":"The Logic of Categories of Partial Functions and its Applications","volume":"241","author":"Obtu\u0142owicz","year":"1986","journal-title":"Diss. Math (Rozprawy Matematyczne)"},{"key":"S0960129500000128_ref017","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"S0960129500000128_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90047-8"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T00:06:10Z","timestamp":1738973170000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000128\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,3]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993,3]]}},"alternative-id":["S0960129500000128"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000128","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[1993,3]]}}}