{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:56:12Z","timestamp":1725796572188},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089171"},{"type":"electronic","value":"9783319089188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08918-8_16","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:44:22Z","timestamp":1404279862000},"page":"224-239","source":"Crossref","is-referenced-by-count":3,"title":["Self Types for Dependently Typed Lambda Encodings"],"prefix":"10.1007","author":[{"given":"Peng","family":"Fu","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L.: A Theory of Primitive Objects - Second-Order Systems. In: European Symposium on Programming (ESOP), pp. 1\u201325 (1994)","DOI":"10.1007\/3-540-57880-3_1"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B.: Wellfounded recursion with copatterns: a unified approach to termination and productivity. In: Morrisett, G., Uustalu, T. (eds.) International Conference on Functional Programming (ICFP), pp. 185\u2013196 (2013)","DOI":"10.1145\/2544174.2500591"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-38946-7_4","volume-title":"Typed Lambda Calculi and Applications","author":"K.Y. Ahn","year":"2013","unstructured":"Ahn, K.Y., Sheard, T., Fiore, M., Pitts, A.M.: System f i . In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol.\u00a07941, pp. 15\u201330. Springer, Heidelberg (2013)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Barendregt, H.: Lambda calculi with types, handbook of logic in computer science. In: Background: Computational Structures, vol.\u00a02 (1993)","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"16_CR5","unstructured":"Barras, B.: Sets in coq, coq in sets. Journal of Formalized Reasoning\u00a03(1) (2010)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science 1(2) (2005)","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Church, A.: The Calculi of Lambda Conversion (AM-6) (Annals of Mathematics Studies) (1985)","DOI":"10.1515\/9781400881932"},{"key":"16_CR8","unstructured":"Coquand, T.: Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA (September 1989)"},{"issue":"2-3","key":"16_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput.\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"16_CR10","unstructured":"Curry, H.B., Hindley, J.R., Seldin, J.P.: Combinatory Logic, vol.\u00a0II (1972)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Fu, P., Stump, A.: Self Types for Dependently Typed Lambda Encodings (2014), Extended version available from http:\/\/homepage.cs.uiowa.edu\/~pfu\/document\/papers\/rta-tlca.pdf","DOI":"10.1007\/978-3-319-08918-8_16"},{"key":"16_CR12","unstructured":"Geuvers, H.: Inductive and Coinductive Types with Iteration and Recursion. In: Nordstrom, B., Petersson, K., Plotkin, G. (eds.) Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 183\u2013207 (1994)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45413-6_16","volume-title":"Typed Lambda Calculi and Applications","author":"H. Geuvers","year":"2001","unstructured":"Geuvers, H.: Induction Is Not Derivable in Second Order Dependent Type Theory. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 166\u2013181. Springer, Heidelberg (2001)"},{"key":"16_CR14","unstructured":"Gimenez, E.: Un calcul de constructions infinies et son application a la verification de systemes communicants. PhD thesis (1996)"},{"key":"16_CR15","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur (1972)"},{"key":"16_CR16","unstructured":"Hickey, J.: Formal objects in type theory using very dependent types. In: Bruce, K. (ed.) In Foundations of Object Oriented Languages (FOOL) 3 (1996)"},{"key":"16_CR17","unstructured":"Mendler, P.: Inductive definition in type theory. Technical report, Cornell University (1987)"},{"key":"16_CR18","unstructured":"Miquel, A.: Le Calcul des Constructions implicite: syntaxe et s\u00e9mantique. PhD thesis, PhD thesis, Universit\u00e9 Paris 7 (2001)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-45070-2_10","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"M. Odersky","year":"2003","unstructured":"Odersky, M., Cremet, V., R\u00f6ckl, C., Zenger, M.: A Nominal Theory of Objects with Dependent Types. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 201\u2013224. Springer, Heidelberg (2003)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-19027-9_10","volume-title":"ESOP \u201988","author":"M. Parigot","year":"1988","unstructured":"Parigot, M.: Programming with Proofs: A Second Order Type Theory. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol.\u00a0300, pp. 145\u2013159. Springer, Heidelberg (1988)"},{"key":"16_CR21","unstructured":"Schepler, D.: Bijective function implies equal types is provably inconsistent with functional extensionality in coq. Message to the Coq Club mailing list (December 12, 2013)"},{"key":"16_CR22","unstructured":"Werner, B.: A Normalization Proof for an Impredicative Type System with Large Elimination over Integers. In: Nordstr\u00f6m, B., Petersson, K., Plotkin, G. (eds.) International Workshop on Types for Proofs and Programs (TYPES), pp. 341\u2013357 (1992)"},{"key":"16_CR23","unstructured":"Werner, B.: Une th\u00e9orie des constructions inductives. PhD thesis, Universit\u00e9 Paris VII (1994)"}],"container-title":["Lecture Notes in Computer Science","Rewriting and Typed Lambda Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08918-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,28]],"date-time":"2024-05-28T14:49:08Z","timestamp":1716907748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08918-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089171","9783319089188"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08918-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}