{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T13:51:33Z","timestamp":1770040293088,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678953","type":"print"},{"value":"9783540446224","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44622-2_21","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:32:38Z","timestamp":1187253158000},"page":"317-331","source":"Crossref","is-referenced-by-count":27,"title":["Interactive Programs in Dependent Type Theory"],"prefix":"10.1007","author":[{"given":"Peter","family":"Hancock","sequence":"first","affiliation":[]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,22]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"L. Augustsson. Cayenne \u2014 a language with dependent types. In Proc. of the International Conference on Functional Programming (ICFP\u201998). ACM Press, September 1998.","DOI":"10.1145\/289423.289451"},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(87)90073-9","volume":"53","author":"L. Halln\u00e4s","year":"1987","unstructured":"L. Halln\u00e4s. An intensional characterization of the largest bisimulation. Theoretical Computer Science, 53:335\u2013343, 1987.","journal-title":"Theoretical Computer Science"},{"key":"21_CR3","unstructured":"P. Hancock and A. Setzer. The IO monad in dependent type theory. DTP\u201999, http:\/\/www.md.chalmers.se\/Cs\/Research\/Semantics\/APPSEM\/dtp99\/proceedings.html , 1999."},{"key":"21_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-59451-5_3","volume-title":"Advanced Functional Programming","author":"J. Hughes","year":"1995","unstructured":"J. Hughes. The design of a pretty-printing library. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, volume 925 of LNCS, pages 53\u201393. Springer, 1995."},{"issue":"1","key":"21_CR5","doi-asserted-by":"publisher","first-page":"57","DOI":"10.2307\/2275015","volume":"54","author":"I. Lindstr\u00f6m","year":"1989","unstructured":"I. Lindstr\u00f6m. A construction of non-well-founded sets within Martin-L\u00f6f\u2019s type theory. Journal of Symbolic Logic, 54(1):57\u201364, 1989.","journal-title":"Journal of Symbolic Logic"},{"key":"21_CR6","first-page":"153","volume-title":"Proceedings 6th Intl. Congress on Logic, Methodology and Philosophy of Science, Hannover, FRG, 22\u201329 Aug 1979","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"P. Martin-L\u00f6f. Constructive mathematics and computer programming. In J. L. Cohen, J. H Lo\u015b, H. Pfeiffer, and K.-D. Podewski, editors, Proceedings 6th Intl. Congress on Logic, Methodology and Philosophy of Science, Hannover, FRG, 22\u201329 Aug 1979, pages 153\u2013175. North Holland, Amsterdam, 1982."},{"key":"21_CR7","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory: Lecture Notes. Bibliopolis, Napoli, 1984."},{"issue":"1","key":"21_CR8","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(1):55\u201392, 1991.","journal-title":"Information and Computation"},{"key":"21_CR9","volume-title":"Programming in Martin-L\u00f6f\u2019 s Type Theory: An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f\u2019 s Type Theory: An Introduction. Clarendon Press, Oxford, 1990."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"S. L. Peyton Jones and P. Wadler. Imperative functional programming. In 20\u2019th ACM Symposium on Principles of Programming Languages, Charlotte, North Carolina, January 1993.","DOI":"10.1145\/158511.158524"},{"key":"21_CR11","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0168-0072(97)00078-X","volume":"92","author":"A. Setzer","year":"1998","unstructured":"A. Setzer. Well-ordering proofs for Martin-L\u00f6f type theory. Annals of Pure and Applied Logic, 92:113\u2013159, 1998.","journal-title":"Annals of Pure and Applied Logic"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"P. Wadler. The essence of functional programming. In 19\u2019th Symposium on Principles of Programming Languages, Albuquerque, volume 19. ACM Press, January 1992.","DOI":"10.1145\/143165.143169"},{"key":"21_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"P. Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, volume 925 of LNCS. Springer Verlag, 1995."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44622-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:17:29Z","timestamp":1556770649000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44622-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678953","9783540446224"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44622-2_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}