{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:07:44Z","timestamp":1725484064792},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432876"},{"type":"electronic","value":"9783540458425"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_5","type":"book-chapter","created":{"date-parts":[[2007,5,27]],"date-time":"2007-05-27T00:00:38Z","timestamp":1180224038000},"page":"63-78","source":"Crossref","is-referenced-by-count":1,"title":["On the Logical Content of Computational Type Theory: A Solution to Curry\u2019s Problem"],"prefix":"10.1007","author":[{"given":"Matt","family":"Fairtlough","sequence":"first","affiliation":[]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"P. Aczel. The Russell-Prawitz modality. Mathematical Structures in Computer Science, 11(4), 2001. Special issue: Modalities in Type Theory (Proceedings of the 1999 Workshop on Intuitionistic Modal Logic and Applications, Trento, Italy).","DOI":"10.1017\/S0960129501003309"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"N. Benton and V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2), March 1998.","DOI":"10.1017\/S0956796898002998"},{"key":"5_CR3","unstructured":"P. N. Benton. A unified approach to strictness analysis and optimising transformations. Technical Report 388, University of Cambridge Computer Laboratory, February 1996."},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"249","DOI":"10.2307\/2266613","volume":"17","author":"H. B. Curry","year":"1952","unstructured":"H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249\u2013265, 1952.","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR5","unstructured":"H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"R. Davies and F. Pfenning. A modal analysis of staged computation. In Jr. Guy Steele, editor, Proc. 23rd POPL. ACM Press, January 1996.","DOI":"10.1145\/237721.237788"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"J. Despeyroux and P. Leleu. Recursion over objects of functional type. Mathematical Structures in Computer Science, 2001.","DOI":"10.1017\/S0960129501003346"},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1997","unstructured":"J. Despeyroux, F. Pfenning, and C. Sch\u00fcrmann. Primitive recursion for higherorder abstract syntax. In Typed Lambda Calculi and Applications, pages 147\u2013163. Springer, 1997. LNCS 1210."},{"issue":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"M. Fairtlough and M. Mendler. Propositional Lax Logic. Information and Computation, 137(1):1\u201333, August 1997.","journal-title":"Information and Computation"},{"key":"5_CR10","unstructured":"M.V.H. Fairtlough and M. Walton. Quantified Lax Logic. Technical Report CS-97-11, Department of Computer Science, The University of Sheffield, July 1997."},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1002\/malq.19810273104","volume":"27","author":"R. I. Goldblatt","year":"1981","unstructured":"R. I. Goldblatt. Grothendieck topology as geometric modality. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik, 27:495\u2013529, 1981.","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1017\/S0960129597002405","volume":"7","author":"J. Hatcli","year":"1997","unstructured":"J. Hatcli. and O. Danvy. A computational formalisation for partial evaluation. Math. Struct. in Comp. Science, 7:507\u2013541, 1997.","journal-title":"Math. Struct. in Comp. Science"},{"key":"5_CR13","unstructured":"B. P. Hilken. Duality for intuitionistic modal algebras. UMCS-96-12-2, Manchester University, Department of Computer Science, 1996. To appear in Journal of Pure and Applied Algebra."},{"key":"5_CR14","unstructured":"P. T. Johnstone. Stone Spaces. Cambridge University Press, 1982."},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF02483860","volume":"12","author":"D. S. Macnab","year":"1981","unstructured":"D. S. Macnab. Modal operators on Heyting algebras. Algebra Universalis, 12:5\u201329, 1981.","journal-title":"Algebra Universalis"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"M. Mendler. Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification. In G. Jones and M. Sheeran, editors, Workshop on Designing Correct Circuits. Springer, 1991.","DOI":"10.1007\/978-1-4471-3544-9_1"},{"key":"5_CR17","unstructured":"M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Department of Computer Science, University of Edinburgh, ECS-LFCS-93-255, March 1993."},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"E. Moggi. Notions of computation and monads. Information and Computation, 93:55\u201392, 1991.","journal-title":"Information and Computation"},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Functional Programming Languages in Education FPLE\u201995","author":"D. A. Turner","year":"1995","unstructured":"D. A. Turner. Elementary strong functional programming. In P. H. Hartel and M. J. Plasmeijer, editors, Functional Programming Languages in Education FPLE\u201995, pages 1\u201313. Springer, 1995. LNCS 1022."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"P. Wadler. Comprehending monads. In Conference on Lisp and Functional Programming. ACM Press, June 1990.","DOI":"10.1145\/91556.91592"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"P. Wadler. Monads for functional programming. In Lecture Notes for the Marktoberdorf Summer School on Program Design Calculi. Springer Verlag, August 1992.","DOI":"10.1007\/978-3-662-02880-3_8"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:03:05Z","timestamp":1556449385000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}