{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:45:20Z","timestamp":1770273920517,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662494974","type":"print"},{"value":"9783662494981","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_10","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:36:06Z","timestamp":1458552966000},"page":"229-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Visible Type Application"],"prefix":"10.1007","author":[{"given":"Richard A.","family":"Eisenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hamidhasan G.","family":"Ahmed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Prog. 23, 552\u2013593 (2013)","journal-title":"J. Funct. Prog."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Buiras, P., Vytiniotis, D., Alejandro Russo, H.: Mixing static and dynamic typing for information-flow control in Haskell. In: International Conference on Functional Programming, ICFP 2015. ACM (2015)","DOI":"10.1145\/2784731.2784758"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Chakravarty, M.M.T., Keller, G., Peyton Jones, S.: Associated type synonyms. In: International Conference on Functional Programming, ICFP 2005. ACM (2005)","DOI":"10.1145\/1086365.1086397"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Chakravarty, M.M.T., Keller, G., Peyton Jones, S., Marlow, S.: Associated types with class. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040306"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, D., Despeyroux, T., Kahn, G., Jo\u00eblle Despeyroux, A.: simple applicative language : Mini-ML. In: Conference on LISP and Functional Programming, LFP 1986. ACM (1986)","DOI":"10.1145\/319838.319847"},{"key":"10_CR6","unstructured":"Coq development team. The Coq proof assistant reference manual. LogiCal Project. Version 8.0 (2004). http:\/\/coq.inria.fr"},{"key":"10_CR7","unstructured":"Damas, L.: Type Assignment in Programming Languages. PhD thesis, University of Edinburgh (1985)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Symposium on Principles of Programming Languages, POPL 1982. ACM (1982)","DOI":"10.1145\/582153.582176"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71316-6_30","volume-title":"Programming Languages and Systems","author":"D Dreyer","year":"2007","unstructured":"Dreyer, D., Blume, M.: Principal type schemes for modular programs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 441\u2013457. Springer, Heidelberg (2007)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higher-rank polymorphism. In: International Conference on Functional Programming, ICFP 2013. ACM (2013)","DOI":"10.1145\/2500365.2500582"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Eisenberg, R.A., Vytiniotis, D., Peyton Jones, S., Weirich, S.: Closed type families with overlapping equations. In: Principles of Programming Languages, POPL 2014. ACM (2014)","DOI":"10.1145\/2535838.2535856"},{"key":"10_CR12","unstructured":"Eisenberg, R.A., Weirich, S., Ahmed, H.: Visible type application (extended version) (2015). http:\/\/www.seas.upenn.edu\/~sweirich\/papers\/type-app-extended.pdf"},{"key":"10_CR13","first-page":"29","volume":"146","author":"JR Hindley","year":"1969","unstructured":"Hindley, J.R.: The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29\u201360 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Le Botlan, D., R\u00e9my, D.: $${\\rm ML}^F$$ ML F : Raising ML to the power of System F. In: International Conference on Functional Programming. ACM (2003)","DOI":"10.1145\/944746.944709"},{"key":"10_CR15","unstructured":"Marlow, S. (ed.): Haskell language report (2010)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"McBride, C.: Agda-curious? Keynote. In: ICFP 2012 (2012)","DOI":"10.1145\/2364527.2364529"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-13346-1_15","volume-title":"Semantics of Data Types","author":"N McCracken","year":"1984","unstructured":"McCracken, N.: The typechecking of programs with implicit type structure. In: Kahn, G., MacQueen, D.B., Plotkin, G. (eds.) Semantics of Data Types. LNCS, vol. 173, pp. 301\u2013315. Springer, Heidelberg (1984)"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR19","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. 2044, pp. 344\u2013359. Springer, Heidelberg (2001)"},{"key":"10_CR20","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden, September 2007"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Odersky, M., L\u00e4ufer, K.: Putting type annotations to work. In: Symposium on Principles of Programming Languages, POPL 1996. ACM (1996)","DOI":"10.1145\/237721.237729"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: International Conference on Functional Programming, ICFP 2006. ACM (2006)","DOI":"10.1145\/1159803.1159811"},{"issue":"1","key":"10_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796806006034","volume":"17","author":"S Peyton Jones","year":"2007","unstructured":"Peyton Jones, S., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitrary-rank types. J. Func. Program. 17(1), 1\u201382 (2007)","journal-title":"J. Func. Program."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"10_CR25","unstructured":"Pottier, F., R\u00e9my, D.: The Essence of ML Type Inference. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 387\u2013489. The MIT Press (2005)"},{"key":"10_CR26","unstructured":"Syme, D.: The F# 2.0 Language Specification. Microsoft Research and the Microsoft Developer Division (2012). http:\/\/fsharp.org\/specs\/language-spec\/2.0\/FSharpSpec-2.0-April-2012.pdf"},{"issue":"4\u20135","key":"10_CR27","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1017\/S0956796811000098","volume":"21","author":"D Vytiniotis","year":"2011","unstructured":"Vytiniotis, D., Peyton Jones, S., Schrijvers, T., Sulzmann, M.: OutsideIn(X) modular type inference with local assumptions. J. Funct. Program. 21(4\u20135), 333\u2013412 (2011)","journal-title":"J. Funct. Program."},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: POPL, pp. 60\u201376. ACM (1989)","DOI":"10.1145\/75277.75283"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-04132-2_2","volume-title":"Practical Aspects of Declarative Languages","author":"T Winant","year":"2014","unstructured":"Winant, T., Devriese, D., Piessens, F., Schrijvers, T.: Partial type signatures for haskell. In: Flatt, M., Guo, H.-F. (eds.) PADL 2014. LNCS, vol. 8324, pp. 17\u201332. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,17]],"date-time":"2020-09-17T09:33:35Z","timestamp":1600335215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}