{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T08:31:56Z","timestamp":1676017916468},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["BIT"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf01995110","type":"journal-article","created":{"date-parts":[[2005,8,10]],"date-time":"2005-08-10T14:40:23Z","timestamp":1123684823000},"page":"84-101","source":"Crossref","is-referenced-by-count":1,"title":["On specifications, subset types and interpretation of proposition in type theory"],"prefix":"10.1007","volume":"32","author":[{"given":"Anne","family":"Salvesen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF01995110_CR1","unstructured":"R. Backhouse,Overcoming the mismatch between programs and proofs. Proceedings of the Workshop on Programming Logic, Marstrand, Sweden, 1987."},{"key":"BF01995110_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundation of Constructive Mathematics","author":"M. J. Beeson","year":"1985","unstructured":"M. J. Beeson,Foundation of Constructive Mathematics, Springer-Verlag Berlin-Heidelberg 1985."},{"key":"BF01995110_CR3","unstructured":"R. Dykhof,Strong elimination rules in type theory. Proceedings of the Workshop on Programming Logic, Marstrand, Sweden, 1987."},{"key":"BF01995110_CR4","unstructured":"S. Hayashi and H. Nakano,PX: A computational Logic, Foundation of Computing Series, MIT Press 1989."},{"issue":"1","key":"BF01995110_CR5","doi-asserted-by":"crossref","first-page":"27","DOI":"10.2307\/2964334","volume":"25","author":"R. Harrop","year":"1960","unstructured":"R. Harrop,Concerning formulas of the types A \u2192 B \u2228 C, A \u2192 (Ex)B(x) in intuitionistic formal series. Journal of Symbolic Logic Vol. 25, No. 1, March 1960, pp. 27\u201332.","journal-title":"Journal of Symbolic Logic"},{"key":"BF01995110_CR6","unstructured":"G. Malcolm and P. Chisholm,Polymorphism and Information Loss in Martin-L\u00f6f's Type Theory. Computing Science Notes, University of Groningen, The Netherlands."},{"key":"BF01995110_CR7","series-title":"Studies in Proof Theory, Lecture Notes","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"P. Martin-L\u00f6f,Intuitionistic Type Theory. Studies in Proof Theory, Lecture Notes, Bibliopolis, Napoli, 1984."},{"key":"BF01995110_CR8","unstructured":"C. Mohring,Extracting F w 's programs from proofs in the calculus of constructions, ACM 1989."},{"key":"BF01995110_CR9","first-page":"915","volume-title":"Types and specifications","author":"B. Nordstr\u00f6m","year":"1983","unstructured":"B. Nordstr\u00f6m and K. Petersson,Types and specifications. In Proceedings IFIP'83, Paris, pp. 915\u2013920. Elsevier, Amsterdam 1983."},{"key":"BF01995110_CR10","unstructured":"B. Nordstr\u00f6m, K. Petersson and J. M. Smith,Programming in Martin-L\u00f6f's Type Theory. An Introduction. Monograph. In preparation. To be published by Oxford University Press."},{"key":"BF01995110_CR11","unstructured":"The Prl Staff (R. Constable et al.),Implementing Mathematics with The Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"BF01995110_CR12","volume-title":"Stable propositions in Martin-L\u00f6f's extensional type theory","author":"A. Salvesen","year":"1989","unstructured":"A. Salvesen,Stable propositions in Martin-L\u00f6f's extensional type theory. In Ph.D. Thesis, University of Oslo, Norway 1989."},{"key":"BF01995110_CR13","doi-asserted-by":"crossref","unstructured":"A. Salvesen and J. M. Smith,The Strength of the Subset Type in Martin-L\u00f6f's Type Theory. Proceedings of the Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, 1988, (IEEE).","DOI":"10.1109\/LICS.1988.5135"},{"key":"BF01995110_CR14","doi-asserted-by":"crossref","unstructured":"J. M. Smith,On a Nonconstructive Type Theory and Program Derivation. To appear in the proceedings of Conference on Logic and its Applications, Bulgaria 1986 (Plenum Press).","DOI":"10.1007\/978-1-4613-0897-3_25"},{"key":"BF01995110_CR15","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1016\/S0049-237X(08)70854-1","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"A. S. Troelstra","year":"1971","unstructured":"A. S. Troelstra,Notions of Realizability. In Proceedings of the Second Scandinavian Logic Symposium, pp. 369\u2013405. North-Holland, Amsterdam, 1971."},{"key":"BF01995110_CR16","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra,Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, No. 344, Springer-Verlag, 1973.","DOI":"10.1007\/BFb0066739"}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995110.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01995110\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T20:25:08Z","timestamp":1586377508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01995110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01995110"],"URL":"https:\/\/doi.org\/10.1007\/bf01995110","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}