{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:00Z","timestamp":1725551940992},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_5","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T23:32:42Z","timestamp":1270855962000},"page":"40-55","source":"Crossref","is-referenced-by-count":21,"title":["\u03a0\u03a3: Dependent Types without the Sugar"],"prefix":"10.1007","author":[{"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils Anders","family":"Danielsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andres","family":"L\u00f6h","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Oury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Altenkirch, T., Oury, N.: \u03a0\u03a3: A core language for dependently typed programming. Draft (2008)"},{"key":"5_CR2","unstructured":"Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter. Draft (2005)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: Proceedings of the 2007 workshop on Programming languages meets program verification, pp. 57\u201368 (2007)","DOI":"10.1145\/1292597.1292608"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne \u2014 a language with dependent types. In: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pp. 239\u2013250 (1998)","DOI":"10.1145\/289423.289451"},{"key":"5_CR5","unstructured":"Chapman, J., Altenkirch, T., McBride, C.: Epigram reloaded: A standalone typechecker for ETT. In: Trends in Functional Programming, vol.\u00a06. Intellect (2006)"},{"key":"5_CR6","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.2 (2009)"},{"key":"5_CR7","unstructured":"Coquand, T.: A calculus of definitions, Draft (2008), http:\/\/www.cs.chalmers.se\/~coquand\/def.pdf"},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1017\/CBO9780511770524.007","volume-title":"From Semantics to Computer Science; Essays in Honour of Gilles Kahn","author":"T. Coquand","year":"2009","unstructured":"Coquand, T., Kinoshita, Y., Nordstr\u00f6m, B., Takeyama, M.: A simple type-theoretic language: Mini-TT. In: From Semantics to Computer Science; Essays in Honour of Gilles Kahn, pp. 139\u2013164. Cambridge University Press, Cambridge (2009)"},{"key":"5_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/11559306_19","volume-title":"Frontiers of Combining Systems","author":"S. Cui","year":"2005","unstructured":"Cui, S., Donnelly, K., Xi, H.: ATS: A language that combines programming with theorem proving. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 310\u2013320. Springer, Heidelberg (2005)"},{"key":"5_CR10","unstructured":"Danielsson, N.A., Altenkirch, T.: Mixing induction and coinduction. Draft (2009)"},{"issue":"1","key":"5_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2005.07.001","volume":"66","author":"P. Dybjer","year":"2006","unstructured":"Dybjer, P., Setzer, A.: Indexed induction-recursion. Journal of Logic and Algebraic Programming\u00a066(1), 1\u201349 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"5_CR12","unstructured":"Gim\u00e9nez, E.: Un Calcul de Constructions Infinies et son Application \u00e0 la V\u00e9rification de Syst\u00e8mes Communicants. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon (1996)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/11780274_27","volume-title":"Algebra, Meaning, and Computation","author":"H. Goguen","year":"2006","unstructured":"Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol.\u00a04060, pp. 521\u2013540. Springer, Heidelberg (2006)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Logical Methods in Computer Science\u00a05(3, 9) (2009)","DOI":"10.2168\/LMCS-5(3:9)2009"},{"key":"5_CR15","unstructured":"McBride, C.: The Strathclyde Haskell Enhancement (2009), http:\/\/personal.cis.strath.ac.uk\/~conor\/pub\/she\/"},{"key":"5_CR16","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and G\u00f6teborg University (2007)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Sheard, T.: Putting Curry-Howard to work. In: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, pp. 74\u201385 (2005)","DOI":"10.1145\/1088348.1088356"},{"key":"5_CR18","unstructured":"Sozeau, M.: Un environnement pour la programmation avec types d\u00e9pendants. PhD thesis, Universit\u00e9 Paris 11 (2008)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Sulzmann, M., Chakravarty, M.M.T., Jones, S.P., Donnelly, K.: System F with type equality coercions. In: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 53\u201366 (2007)","DOI":"10.1145\/1190315.1190324"},{"key":"5_CR20","unstructured":"Wadler, P., Taha, W., MacQueen, D.: How to add laziness to a strict language, without even being odd. In: The 1998 ACM SIGPLAN Workshop on ML (1998)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:52:01Z","timestamp":1606186321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}