{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:30:15Z","timestamp":1707521415635},"reference-count":26,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.43.2","type":"journal-article","created":{"date-parts":[[2010,12,21]],"date-time":"2010-12-21T02:02:48Z","timestamp":1292896968000},"page":"14-28","source":"Crossref","is-referenced-by-count":22,"title":["MiniAgda: Integrating Sized and Dependent Types"],"prefix":"10.4204","volume":"43","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[{"name":"Ludwig-Maximilians-University Munich"}]}],"member":"2720","published-online":{"date-parts":[[2010,12,21]]},"reference":[{"key":"abel:PhD","volume-title":"A Polymorphic Lambda-Calculus with Sized Higher-Order Types","author":"Andreas Abel","year":"2006"},{"issue":"2","key":"abel:lmcs07","article-title":"Semi-continuous Sized Types and Termination","volume":"4","author":"Andreas Abel","year":"2008","journal-title":"Logical Methods in Computer Science"},{"issue":"8","key":"abel:scp09","doi-asserted-by":"crossref","first-page":"550","DOI":"10.1016\/j.scico.2008.01.004","article-title":"Type-Based Termination of Generic Programs","volume":"74","author":"Andreas Abel","year":"2009","journal-title":"Science of Computer Programming"},{"issue":"1","key":"abelalti:predicative","first-page":"1","article-title":"A Predicative Analysis of Structural Recursion","volume":"12","author":"Andreas Abel","year":"2002","journal-title":"Journal of Functional Programming"},{"key":"DBLP:conf\/fossacs\/2008","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings","volume":"4962","year":"2008"},{"key":"barrasBernardo:fossacs08","first-page":"365","article-title":"The Implicit Calculus of Constructions as a Programming Language with Dependent Types","author":"Bruno Barras","year":"2008"},{"issue":"1","key":"gimenez:typeBased","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1017\/S0960129503004122","article-title":"Type-Based Termination of Recursive Definitions","volume":"14","author":"Gilles Barthe","year":"2004","journal-title":"Mathematical Structures in Computer Science"},{"key":"bartheGregoirePastawski:lpar06","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/11916277_18","article-title":"CIC^: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings","volume":"4246","author":"Gilles Barthe","year":"2006"},{"key":"bertotKomendantskaya:types08","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-642-02444-3_14","article-title":"Using Structural Recursion for Corecursion","volume-title":"Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers","volume":"5497","author":"Yves Bertot","year":"2008"},{"key":"blanqui:rta04","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-540-25979-4_2","article-title":"A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems","volume-title":"Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3 -- 5, 2004, Proceedings","volume":"3091","author":"Fr\u00e9d\u00e9ric Blanqui","year":"2004"},{"key":"blanqui:csl05","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/11538363_11","article-title":"Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations.","volume-title":"Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings","volume":"3634","author":"Fr\u00e9d\u00e9ric Blanqui","year":"2005"},{"key":"bradyMcBrideMcKinna:types03","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-540-24849-1_8","article-title":"Inductive Families Need Not Store Their Indices","volume-title":"Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers","volume":"3085","author":"Edwin Brady","year":"2004"},{"key":"coquand:infiniteobjects","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","article-title":"Infinite Objects in Type Theory","volume-title":"Types for Proofs and Programs (TYPES '93)","volume":"806","author":"Thierry Coquand","year":"1993"},{"key":"danielsson:beating","volume-title":"Beating the Productivity Checker Using Embedded Languages","author":"Nils Anders Danielsson","year":"2010"},{"key":"gimenez:guardeddefinitions","series-title":"LNCS","first-page":"39","article-title":"Codifying Guarded Definitions with Recursive Schemes","volume-title":"Types for Proofs and Programs, International Workshop TYPES'94, Br astad, Sweden, June 6-10, 1994, Selected Papers","volume":"996","author":"Eduardo Gim\u00e9nez","year":"1995"},{"key":"hughesParetoSabry:popl96","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1145\/237721.240882","article-title":"Proving the Correctness of Reactive Systems Using Sized Types","volume-title":"23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'96","author":"John Hughes","year":"1996"},{"key":"inria:coq82","volume-title":"The Coq Proof Assistant Reference Manual","author":"INRIA","year":"2008"},{"key":"jones:sizeChange","first-page":"81","article-title":"The Size-Change Principle for Program Termination","volume-title":"ACM Symposium on Principles of Programming Languages (POPL'01)","author":"Chin Soon Lee","year":"2001"},{"key":"mcBrideMcKinna:view","article-title":"The View from the Left","author":"Conor McBride","year":"2004","journal-title":"Journal of Functional Programming"},{"key":"mehltretter:diploma","volume-title":"Termination Checking for a Dependently Typed Language","author":"Karl Mehltretter","year":"2007"},{"key":"miquel:tlca01","series-title":"Lecture Notes in Computer Science","first-page":"344","article-title":"The Implicit Calculus of Constructions","volume-title":"Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings","volume":"2044","author":"Alexandre Miquel","year":"2001"},{"key":"mishraLingerSheard:fossacs08","first-page":"350","article-title":"Erasure and Polymorphism in Pure Type Systems","author":"Nathan Mishra-Linger","year":"2008"},{"key":"mishraLinger:PhD","volume-title":"Irrelevance, Polymorphism, and Erasure in Type Theory","author":"Richard Nathan Mishra-Linger","year":"2008"},{"key":"norell:PhD","volume-title":"Towards a Practical Programming Language Based on Dependent Type Theory","author":"Ulf Norell","year":"2007"},{"key":"wahlstedt:PhD","volume-title":"Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion","author":"David Wahlstedt","year":"2007"},{"issue":"1","key":"xi:terminationHOSC","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/A:1019916231463","article-title":"Dependent Types for Program Termination Verification","volume":"15","author":"Hongwei Xi","year":"2002","journal-title":"Journal of Higher-Order and Symbolic Computation"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,3,6]],"date-time":"2019-03-06T16:34:59Z","timestamp":1551890099000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1012.4896v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,21]]},"references-count":26,"URL":"https:\/\/doi.org\/10.4204\/eptcs.43.2","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,21]]}}}