{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:27:18Z","timestamp":1725492438121},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665373"},{"type":"electronic","value":"9783540481676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48167-2_4","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T07:40:19Z","timestamp":1191570019000},"page":"47-62","source":"Crossref","is-referenced-by-count":1,"title":["A Modal Lambda Calculus with Iteration and Case Constructs"],"prefix":"10.1007","author":[{"given":"Jo\u00eblle","family":"Despeyroux","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Leleu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"4_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proceedings TLCA","author":"Y. Akama","year":"1993","unstructured":"Y. Akama. On Mints\u2019 reduction for ccc-calculus. In Proceedings TLCA, pages 1\u201312. Springer-Verlag LNCS 664, 1993. 54"},{"key":"4_CR2","unstructured":"Gavin Bierman and Valeria de Paiva. Intuitionistic necessity revisited. In Technical Report CSRP-96-10, School of Computer Science, University of Birmingham, June 1996. 48"},{"key":"4_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings ICALP\u201993","author":"R. Cosmo Di","year":"1993","unstructured":"R. Di Cosmo and D. Kesner. A Confluent Reduction for the Extensional Typed \u03bb-calculus. In Proceedings ICALP\u201993. Springer-Verlag LNCS 700, 1993. 54"},{"key":"4_CR4","unstructured":"J. Despeyroux and A. Hirschowitz. Higher-order syntax and induction in coq. In F. Pfenning, editor, Proceedings of the fifth Int. Conf. on Logic Programming and Automated Reasoning (LPAR 94), Kiev, Ukraine, July 16\u201321, 1994, volume 822. Springer-Verlag LNAI, 1994. 50, 53, 59"},{"key":"4_CR5","unstructured":"Jo\u00eblle Despeyroux and Pierre Leleu. Primitive recursion for higher-order abstract syntax-dependant types. Draft, submitted for publication, 1999. 60"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Jr. Guy Steele, editor, Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, pages 258\u2013270, St. Petersburg Beach, Florida, January 1996. ACM Press. 48","DOI":"10.1145\/237721.237788"},{"key":"4_CR7","unstructured":"Jo\u00eblle Despeyroux, Frank Pfenning, and Carsten Sch\u00fcrmann. Primitive recursion for higher-order abstract syntax. Technical Report CMU-CS-96-172, Carnegie Mellon University, September 1996. 52"},{"key":"4_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"Int. Conf. on Typed lambda calculi and applications-TLCA\u201997","author":"J. Despeyroux","year":"1997","unstructured":"Jo\u00eblle Despeyroux, Frank Pfenning, and Carsten Sch\u00fcrmann. Primitive Recursion for Higher-Order Abstract Syntax. In J.R. Hindley and P. de Groote, editors, Int. Conf. on Typed lambda calculi and applications-TLCA\u201997, pages 147\u2013163, Nancy, France, April 1997. Springer-Verlag LNCS 1210. 47, 48, 49, 53, 59, 60"},{"key":"4_CR9","unstructured":"Neil Ghani. Eta Expansions in System F. Technical Report LIENS-96-10, LIENS-DMI, Ecole Normale Superieure, 1996. 48, 55, 56"},{"key":"4_CR10","unstructured":"Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989. 56"},{"issue":"1","key":"4_CR11","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993. 48, 49","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. Semantical analysis of higher-order abstract syntax. In IEEE, editor, Proceedings of the International Conference on Logic In Computer Sciences, LICS, 1999. 59, 60","DOI":"10.1109\/LICS.1999.782616"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C.B. Jay","year":"1995","unstructured":"C.B. Jay and N. Ghani. The Virtues of Eta-Expansion. Journal of Functional Programming, 5(2):135\u2013154, April 1995. 48, 54, 56","journal-title":"Journal of Functional Programming"},{"key":"4_CR14","unstructured":"Pierre Leleu. A Modal Lambda Calculus with Iteration and Case Constructs. Technical Report RR-3322, INRIA, France, December 1997. http:\/\/www.inria.fr\/RRRT\/RR-3322.html . 48, 52, 57, 58"},{"key":"4_CR15","unstructured":"Pierre Leleu. Metatheoretic Results for a Modal Lambda Calculus. Technical Report RR-3361, INRIA, France, 1998. http:\/\/www.inria.fr\/RRRT\/RR-3361.html . 54"},{"key":"4_CR16","unstructured":"Pierre Leleu. Syntaxe abstraite d\u2019ordre sup\u00e9rieur et r\u00e9cursion dans les th\u00e9ories typ\u00e9es. Phd thesis, Ecole Nationale des Ponts et Chauss\u00e9es (ENPC), December 1998. In French. 60"},{"key":"4_CR17","unstructured":"Zhaohui Luo. Computation and Reasoning. Oxford University Press, 1994. 49"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Proceedings of LICS\u201997, pages 434\u2013445, Warsaw, 1997. 59","DOI":"10.1109\/LICS.1997.614968"},{"key":"4_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for Proofs and Programs","author":"L. Magnusson","year":"1994","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 213\u2013237. Springer-Verlag LNCS 806, 1994. 60"},{"issue":"2","key":"4_CR20","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M.H.A. Newman","year":"1942","unstructured":"M.H.A. Newman. On theories with a combinatorial definition of \u2018equivalence\u2019. Ann. Math., 43(2):223\u2013243, 1942. 58","journal-title":"Ann. Math."},{"key":"4_CR21","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f\u2019 s Type Theory: An Introduction. Oxford University Press, 1990. 47, 60"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN\u2019 88 Symposium on Language Design and Implementation, pages 199\u2013208, Atlanta, Georgia, June 1988. 47","DOI":"10.1145\/53990.54010"},{"key":"4_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Int. Conf. on Typed Lambda Calculi and Applications, TLCA\u201993","author":"Ch. Paulin-Mohring","year":"1992","unstructured":"Ch. Paulin-Mohring. Inductive definitions in the system coq. rules and properties. In J.F. Groote M. Bezem, editor, Proceedings of the Int. Conf. on Typed Lambda Calculi and Applications, TLCA\u201993, Springer-Verlag LNCS 664, 1992. 47"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. Automated Theorem Proving in a Simple Meta Logic for LF. In Proceedings of the CADE-15 Conference, Lindau-Germany, July 1998. 59","DOI":"10.1007\/BFb0054266"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Hao-Chi Wong. On a modal \u03bb-calculus for S4. In S. Brookes and M. Main, editors, Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Sematics, New Orleans, Louisiana, March 1995. To appear in Electronic Notes in Theoretical Computer Science, Volume 1, Elsevier. 48, 49, 51, 52","DOI":"10.1016\/S1571-0661(04)00028-3"},{"key":"4_CR26","unstructured":"Benjamin Werner. Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7, 1994. 47, 49, 55"}],"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-48167-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T09:57:08Z","timestamp":1684058228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48167-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665373","9783540481676"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48167-2_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}