{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300698,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540571827"},{"type":"electronic","value":"9783540479277"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57182-5_3","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:09:50Z","timestamp":1330258190000},"page":"32-67","source":"Crossref","is-referenced-by-count":19,"title":["Deliverables: a categorical approach to program development in type theory"],"prefix":"10.1007","author":[{"given":"James","family":"McKinna","sequence":"first","affiliation":[]},{"given":"Rod","family":"Burstall","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"J.B\u00e9nabou, Fibred categories and the foundations of na\u00efve category theory, JSL, 1985.","DOI":"10.2307\/2273784"},{"key":"3_CR2","volume-title":"Ph.D. thesis","author":"S. Berardi","year":"1990","unstructured":"S. Berardi, Type Dependence and Constructive Mathematics, Ph.D. thesis, Dipartimento di Informatica, Torino, Italy 1990."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn, A survey of the project AUTOMATH, in: [35].","DOI":"10.1016\/S0049-237X(08)70203-9"},{"key":"3_CR4","unstructured":"R.M.Burstall and J.H.McKinna, Deliverables: an approach to program development in Constructions, in [15], also available as a University of Edinburgh technical report ECS-LFCS-91-133."},{"key":"3_CR5","volume-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"R. Constable","year":"1986","unstructured":"R.Constable et al., Implementing Mathematics with the NuPrl Proof Development System, Prentice-Hall, New Jersey, 1986."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"T.Coquand and G.Huet, Constructions: a Higher-order Proof system for mechanizing mathematics, in: Proceedings EUROCAL '85, LNCS 203, Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"3_CR7","volume-title":"Rapports Techniques no.110, Projet Formel","author":"T. Coquand","year":"1989","unstructured":"T.Coquand, Metamathematical Investigations of a Calculus of Constructions, in: [14]."},{"key":"3_CR8","volume-title":"Pitman Research Notes in Theoretical Computer Science","author":"P-L. Curien","year":"1986","unstructured":"P-L.Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman Research Notes in Theoretical Computer Science, Pitman, London, 1986."},{"key":"3_CR9","unstructured":"J-Y.Girard, Interpretation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique de l'ordre sup\u00e9rieure, thesis, University of Paris VII, 1972."},{"key":"3_CR10","volume-title":"Theoretical Computer Science, Vol. 41","author":"S. Hayashi","year":"1985","unstructured":"S.Hayashi, Adjunction of semifunctors: categorical structures in nonextensional lambda calculus, in Theoretical Computer Science, Vol. 41, North-Holland, Amsterdam, 1985."},{"key":"3_CR11","series-title":"Springer LNCS 526","volume-title":"Proceedings of TACS '91","author":"S. Hayashi","year":"1991","unstructured":"S.Hayashi, Singleton, Union and Intersection Types for Program Extraction, in: Proceedings of TACS '91, Sendai, Japan, Springer LNCS 526, Springer-Verlag, 1991."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"C.A.R.Hoare, An axiomatic basis for computer programming, in: Communications of the ACM, Vol. 12, 1969.","DOI":"10.1145\/363235.363259"},{"key":"3_CR13","unstructured":"W.A.Howard, The \u201cformulae-as-types\u201d notion of construction, in: [35]."},{"key":"3_CR14","volume-title":"Rapports Techniques no.110, Projet Formel","author":"G. Huet","year":"1989","unstructured":"G.Huet, T.Coquand, C.Paulin-Mohring et al., The Calculus of Constructions, Version 4-10, Documentation and user's manual, Rapports Techniques no.110, Projet Formel, INRIA-Rocquencourt, Paris, August 1989."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"G.Huet and G.Plotkin, eds. Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks, Antibes, May 1990, distributed electronically to participating BRA sites, January 1991.","DOI":"10.1017\/CBO9780511569807"},{"key":"3_CR16","unstructured":"J.M.E.Hyland and A.M.Pitts, The Theory of Constructions: Categorical Semantics and Topos-theoretic models, in: Proceedings of the AMS Conference on Categories in Computer Science, Boulder, Colorado, 1986."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"P.T.Johnstone and R.Par\u00e9, eds., Indexed Categories and their Applications, Springer LNM 661, Springer-Verlag, 1978.","DOI":"10.1007\/BFb0061360"},{"key":"3_CR18","volume-title":"Cambridge Studies in Advanced Mathematics no. 7","author":"J. Lambek","year":"1986","unstructured":"J.Lambek and P.J.Scott, An Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics no. 7, Cambridge University Press, Cambridge, England, 1986."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Z.Luo, ECC, an Extended Calculus of Constructions, in: Proceedings of the Fourth IEEE Conference on Logic in Computer Science, Asilomar, California, 1989.","DOI":"10.1109\/LICS.1989.39193"},{"key":"3_CR20","unstructured":"Z.Luo, An Extended Calculus of Constructions, Ph.D. Thesis, Department of Computer Science, University of Edinburgh, June 1990."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Z.Luo, Program Specification and Data Refinement in Type Theory, Technical Report ECS-LFCS-90-131, Department of Computer Science, University of Edinburgh, January 1991.","DOI":"10.1007\/3-540-53982-4_9"},{"key":"3_CR22","unstructured":"Z.Luo and R.Pollack, LEGO Proof Development System: User's Manual, LFCS Technical Report ECS-LFCS-92-211, 1992."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"J.H.McKinna, Deliverables: a categorical approach to program development in type theory, Ph.D. thesis, University of Edinburgh, 1992.","DOI":"10.1007\/3-540-57182-5_3"},{"key":"3_CR24","volume-title":"Logic Colloquium 73","author":"P. Martin-L\u00f6f","year":"1975","unstructured":"P.Martin-L\u00f6f, An Intuitionistic Theory of Types: Predicative part, in: Logic Colloquium 73, North-Holland, Amsterdam, 1975."},{"key":"3_CR25","volume-title":"Constructive Mathematics and Computer Programming","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"P.Martin-L\u00f6f, Constructive Mathematics and Computer Programming, in: proceedings of the Conference on Logic, Philosophy and Methodology of Science VI, 1979, North-Holland, Amsterdam, 1982."},{"key":"3_CR26","unstructured":"M.Mendler, The Logic of Design, Ph.D. thesis, University of Edinburgh, forthcoming, 1992."},{"key":"3_CR27","unstructured":"B.Nordstr\u00f6m, K.Petersson, and J.Smith, Programming in Martin-L\u00f6f's type theory, Oxford University Press, 1990."},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"C.Paulin-Mohring, Extracting F \u03c9 's programs from proofs in the Calculus of Constructions, in: Proceedings POPL89, ACM, 1989.","DOI":"10.1145\/75277.75285"},{"key":"3_CR29","unstructured":"C.Paulin-Mohring and B.Werner, Extracting and Executing Programs developed in the Inductive Constructions System: a Progress Report, in: [15]."},{"key":"3_CR30","unstructured":"D.Pavlovi\u010d, Predicates and Fibrations, proefschrift, University of Utrecht, 1990."},{"key":"3_CR31","unstructured":"R.A.Pollack, Implicit Syntax, in: [15]."},{"key":"3_CR32","unstructured":"A.Salvesen and J.Smith, On the strength of the subset type in Martin-L\u00f6fs type theory, in: Proceedings of the Third LICS Symposium, IEEE, 1988."},{"key":"3_CR33","unstructured":"A.Salvesen, On Information Discharging and Retrieval in Martin-L\u00f6f's type theory, Ph.D. thesis, Institute of Informatics, University of Oslo, 1989."},{"key":"3_CR34","unstructured":"D.Sannella, Formal specification of ML programs, LFCS technical report ECS-LFCS-86-15, Dept. of Computer Science, University of Edinburgh, 1986."},{"key":"3_CR35","unstructured":"J.P.Seldin and J.R.Hindley, eds., To H.B.Curry, essays in Combinatory Logic, \u03bb-calculus and Formalism, Academic Press, 1980."},{"key":"3_CR36","unstructured":"B.Reus and T.Streicher, Verifying Properties of Module Constructions in Type Theory, this volume."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1993"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57182-5_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:01:23Z","timestamp":1742594483000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57182-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540571827","9783540479277"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-57182-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}