{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:17:01Z","timestamp":1770293821846,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540784975","type":"print"},{"value":"9783540784999","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78499-9_25","type":"book-chapter","created":{"date-parts":[[2008,4,1]],"date-time":"2008-04-01T23:02:25Z","timestamp":1207090945000},"page":"350-364","source":"Crossref","is-referenced-by-count":21,"title":["Erasure and Polymorphism in Pure Type Systems"],"prefix":"10.1007","author":[{"given":"Nathan","family":"Mishra-Linger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Sheard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr"},{"issue":"1\u20132","key":"25_CR2","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0304-3975(93)90082-5","volume":"121","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. Theoretical Computer Science\u00a0121(1\u20132), 9\u201358 (1993)","journal-title":"Theoretical Computer Science"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne \u2013 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":"25_CR4","volume-title":"Handbook of Logic in Computer Science","author":"H.P. Barendregt","year":"1992","unstructured":"Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, Oxford University Press, Oxford (1992)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"key":"25_CR6","unstructured":"Brady, E.: Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham (2005)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Chen, C., Xi, H.: Combining programming with theorem proving. In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pp. 66\u201377 (2005)","DOI":"10.1145\/1086365.1086375"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 42\u201354 (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"25_CR9","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1109\/TASE.2007.28","volume-title":"First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering","author":"C. Lin","year":"2007","unstructured":"Lin, C., McCreight, A., Shao, Z., Chen, Y., Guo, Y.: Foundational typed assembly language with certified garbage collection. In: First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering, pp. 326\u2013338. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"25_CR10","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and reasoning: A type theory for computer science","author":"Z. Luo","year":"1994","unstructured":"Luo, Z.: Computation and reasoning: A type theory for computer science. Oxford University Press, New York, USA (1994)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3540543961_15","volume-title":"Functional Programming Languages and Computer Architecture","author":"H.G. Mairson","year":"1991","unstructured":"Mairson, H.G.: Outline of a proof theory of parametricity. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol.\u00a0523, pp. 313\u2013327. Springer, Heidelberg (1991)"},{"issue":"1","key":"25_CR12","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming\u00a014(1), 69\u2013111 (2004)","journal-title":"Journal of Functional Programming"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-45413-6_27","volume-title":"Typed Lambda Calculi and Applications","author":"A. Miquel","year":"2001","unstructured":"Miquel, A.: The implicit calculus of constructions. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 344\u2013359. Springer, Heidelberg (2001)"},{"key":"25_CR14","unstructured":"Miquel, A.: Le Calcul des Constructions Implicite: Syntaxe et S\u00e9mantique. PhD thesis, Universit\u00e9 Paris 7 (2001)"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Peyton-Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (2006)","DOI":"10.1145\/1159803.1159811"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/LICS.2001.932499","volume-title":"LICS 2001: Proceedings of the 16th Annual Symposium on Logic in Computer Science","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: LICS 2001: Proceedings of the 16th Annual Symposium on Logic in Computer Science, pp. 221\u2013230. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G.D. Plotkin","year":"1993","unstructured":"Plotkin, G.D., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 361\u2013375. Springer, Heidelberg (1993)"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Sheard, T.: Languages of the future. In: Proceedings of the Nineteenth ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA Companion Volume, pp. 116\u2013119 (2004)","DOI":"10.1145\/1028664.1028711"},{"key":"25_CR20","unstructured":"Sheard, T., Pa\u0161ali\u0107, E.: Meta-programming with built-in type equality. In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), pp. 106\u2013124 (2004), http:\/\/cs-www.cs.yale.edu\/homes\/carsten\/lfm04\/"},{"key":"25_CR21","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1145\/99370.99404","volume-title":"Functional Programming Languages and Computer Architecture","author":"P. Wadler","year":"1989","unstructured":"Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, pp. 347\u2013359. ACM Press, New York (1989)"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78499-9_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,24]],"date-time":"2024-02-24T09:57:49Z","timestamp":1708768669000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78499-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540784975","9783540784999"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78499-9_25","relation":{},"subject":[]}}