{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:50Z","timestamp":1761611150169,"version":"3.32.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1992,9,1]],"date-time":"1992-09-01T00:00:00Z","timestamp":715305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1992,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The calculus of constructions of Coquand, which is a version of higher order typed<jats:italic>\u03bb<\/jats:italic>-calculus based on the dependent function type, is considered from the perspective of its use as the mathematical foundation for a proof development system. The paper considers formulations of the calculus, the underlying consistency of the formalism (i.e., the strong normalisation theorem), and the proof theory of adding assumptions for notions from logic and set theory. Proofs are not given, but references to them are.<\/jats:p>","DOI":"10.1007\/bf01211392","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:14:33Z","timestamp":1109369673000},"page":"425-441","source":"Crossref","is-referenced-by-count":5,"title":["Coquand's calculus of constructions: A mathematical foundation for a proof development system"],"prefix":"10.1145","volume":"4","author":[{"given":"Jonathan P.","family":"Seldin","sequence":"first","affiliation":[{"name":"Department of Mathematics, Concordia University, 7141 Sherbrooke Street West, H4B 1R6, Montr\u00e9al, Qu\u00e9bec, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"volume-title":"A Transfinite Type Theory with Type Variables","year":"1965","author":"Andrews P. B.","key":"e_1_2_1_2_1_2"},{"volume-title":"Implementing Mathematics with the Nuprl Proof Development System","year":"1986","author":"Constable R.","key":"e_1_2_1_2_2_2"},{"key":"e_1_2_1_2_3_2","first-page":"123","volume-title":"Logic Colloquium '85: Proceedings of the Colloquium Held in Orsay, July 7\u201313, 1985","author":"Coquand T.","year":"1986"},{"key":"e_1_2_1_2_4_2","first-page":"151","volume-title":"EUROCAL85, Vol. 203","author":"Coquand T.","year":"1986"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_2_6_2","unstructured":"Coquand T.: Une Th\u00e9orie des Constructions. PhD Thesis University of Paris VII 1985."},{"key":"e_1_2_1_2_7_2","unstructured":"Coquand T.: An Analysis of Girard's Paradox. In: Symp. on Logic in Computer Science pp. 227\u2013236. IEEE Computer Society IEEE Computer Society Press 1986."},{"key":"e_1_2_1_2_8_2","unstructured":"Coquand T.: Metamathematical Investigations of a Calculus of Constructions. February 9 1987. Privately circulated 1987."},{"volume-title":"Foundations of Mathematical Logic","year":"1963","author":"Curry H. B.","key":"e_1_2_1_2_9_2"},{"volume-title":"Combinatory Logic, Vol. 1","year":"1958","author":"Curry H. B.","key":"e_1_2_1_2_10_2"},{"volume-title":"Combinatory Logic, volume 2","year":"1972","author":"Curry H. B.","key":"e_1_2_1_2_11_2"},{"key":"e_1_2_1_2_12_2","unstructured":"Daalen D. T. van: The Language Theory of AUTOMATH. PhD Thesis Technische Hogeschool Eindhoven February 1980."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"volume-title":"Symbolic Logic","year":"1952","author":"Fitch F. B.","key":"e_1_2_1_2_14_2"},{"key":"e_1_2_1_2_15_2","unstructured":"Girard J.-Y.: Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de L'Arithm\u00e9tique d'Orde Sup\u00e9rieur. PhD Thesis University of Paris VII 1972."},{"key":"e_1_2_1_2_16_2","unstructured":"Hindley J. R. and Seldin J. P.: Introduction to Combinators and \u03bb-calculus . Cambridge University Press 1986."},{"key":"e_1_2_1_2_17_2","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard W. A.","year":"1980"},{"key":"e_1_2_1_2_18_2","unstructured":"Huet G.: Formal Structures for Computation and Deduction. Course Notes Carnegie-Mellon University First Edition May 1986."},{"key":"e_1_2_1_2_19_2","first-page":"276","volume-title":"TAPSOFT '87: Proc. International Joint Conf. on Theory and Practice of Software Development, Pisa, Italy, March 23\u201327, 1987. Vol. 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP '87)","author":"Huet G.","year":"1987"},{"key":"e_1_2_1_2_20_2","unstructured":"Korelsky T. Dean W. Eichenlaub C. Hook J. Klapper C. Lam M. McCullough D Brooke-McFarland C. Pottinger G. Rambow O. Rosenthal D. Seldin J. P. and Weber D. G.: Ulysses: A Computer-Security Modeling Environment. In Proc. 11th National Computer Security Conf. Baltimore Maryland October 17\u201320 1988 pp. 20\u201328. National Bureau of Standards and National Computer Security Center October 1988."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Korelsky T. Dean W. Eichenlaub C. Hook J. Klapper C. Lam M. McCullough D. Pottinger G. Rambow O. Rosenthal D. Seldin J. P. and Weber D.G.: Security Modelling in the Ulysses Environment. In Proc. Fourth Aerospace Computer Security Applications Conf. Orlando Florida December 12\u201316 1988 pp. 386\u2013392. IEEE Computer Society Press December 1988.","DOI":"10.1109\/ACSAC.1988.113337"},{"key":"e_1_2_1_2_22_2","unstructured":"Luo Z.: ECC an Extended Calculus of Constructions. In Proc. Fourth Annual Symp. on Logic in Computer Science June 1989 Asilomar California USA 1989."},{"key":"e_1_2_1_2_23_2","unstructured":"Luo Z.: An Extended Calculus of Constructions. PhD Thesis University of Edinburgh 1990."},{"key":"e_1_2_1_2_24_2","unstructured":"Martin-L\u00f6f P.: A Theory of Types. Revised October 1971. Privately circulated February 1971."},{"key":"e_1_2_1_2_25_2","first-page":"73","volume-title":"Logic Colloquium '73","author":"Martin-L\u00f6f P.","year":"1975"},{"key":"e_1_2_1_2_26_2","first-page":"153","volume-title":"Logic, Methodology and Philosophy of Science VI","author":"Martin-L\u00f6f P.","year":"1982"},{"key":"e_1_2_1_2_27_2","unstructured":"Martin-L\u00f6f P.: Intuitionistic Type Theory. Bibliopolis Naples 1984. Notes by G. Sambin of a series of lectures given in Padua June 1980."},{"key":"e_1_2_1_2_28_2","unstructured":"Nederpelt R. P.: Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types. PhD Thesis Technical University of Eindhoven 1973."},{"key":"e_1_2_1_2_29_2","unstructured":"Pottinger G.: Strong Normalization for Terms of the Theory of Constructions. Technical Report TR 11-7 Odyssey Research Associates December 1987."},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-94-009-0681-5_14","volume-title":"Truth or Consequences: Essays in Honor of Nuel Belnap","author":"Pottinger G.","year":"1990"},{"volume-title":"Natural Deduction","year":"1965","author":"Prawitz D.","key":"e_1_2_1_2_31_2"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.2307\/2272314"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Seldin J. P.: MATHESIS: The Mathematical Foundation for ULYSSES. Interim Report RADC-TR-87-223 RADC November 1987. (Published 1988.)","DOI":"10.21236\/ADA195379"},{"key":"e_1_2_1_2_34_2","unstructured":"Seldin J. P.: Excluded Middle Without Definite Descriptions in the Theory of Constructions. Extended Abstract. Proc. of the First Montr\u00e9al Workshop on Programming Language Theory Concordia University Montr\u00e9al April 29\u201330 1991 M. Okada and P. J. Scott (eds) pp. 74\u201383 Concordia University Centre for Pattern Recognition and Machine Intelligence Montr\u00e9al 1991."},{"key":"e_1_2_1_2_35_2","unstructured":"Seldin J. P.: On the Proof Theory of Coquand's Calculus of Constructions. In preparation."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211392.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211392\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T03:47:36Z","timestamp":1735012056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1992,9]]}},"alternative-id":["10.1007\/BF01211392"],"URL":"https:\/\/doi.org\/10.1007\/bf01211392","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}