{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:48Z","timestamp":1779836748841,"version":"3.53.1"},"reference-count":28,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2013,10,22]],"date-time":"2013-10-22T00:00:00Z","timestamp":1382400000000},"content-version":"unspecified","delay-in-days":174,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper presents a library for programming with polymorphic dynamic types in the dependently typed programming language Agda. The resulting library allows dynamically typed values with a\n                    <jats:italic>polymorphic type<\/jats:italic>\n                    to be instantiated to a less general (possibly monomorphic) type without compromising type soundness.\n                  <\/jats:p>","DOI":"10.1017\/s0956796813000063","type":"journal-article","created":{"date-parts":[[2013,10,22]],"date-time":"2013-10-22T07:39:24Z","timestamp":1382427564000},"page":"229-248","source":"Crossref","is-referenced-by-count":1,"title":["A library for polymorphic dynamic typing"],"prefix":"10.1017","volume":"23","author":[{"given":"WOUTER","family":"SWIERSTRA","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"THOMAS","family":"VAN NOORT","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,10,22]]},"reference":[{"key":"S0956796813000063_ref22","volume-title":"Proceedings of the International Conference on Functional Programming (ICFP '08)","author":"Oury","year":"2008"},{"key":"S0956796813000063_ref17","doi-asserted-by":"crossref","unstructured":"McBride C. (2010) Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming (WGP '10).","DOI":"10.1145\/1863495.1863497"},{"key":"S0956796813000063_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.012"},{"key":"S0956796813000063_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796813000063_ref4","volume-title":"Proceedings of the International Conference on Functional Programming (ICFP '02)","author":"Baars","year":"2002"},{"key":"S0956796813000063_ref6","volume-title":"Proceedings of the 12th International Conference on Trends in Functional Programming (TFP '11)","author":"Brady","year":"2011"},{"key":"S0956796813000063_ref8","volume-title":"Proceedings of the 15th ACM Sigplan International Conference on Functional Programming (ICFP '10)","author":"Chapman","year":"2010"},{"key":"S0956796813000063_ref9","volume-title":"Proceedings of the Haskell Workshop (Haskell '02)","author":"Cheney","year":"2002"},{"key":"S0956796813000063_ref10","unstructured":"Danielsson N. A. (2006) A formalisation of a dependently typed language as an inductive-recursive family. Proceedings of the Types for Proofs and Programs Conference (TYPES '06)."},{"key":"S0956796813000063_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004957"},{"key":"S0956796813000063_ref7","unstructured":"Chapman J. (2008) Type Checking and Normalisation, PhD thesis, University of Nottingham, Nottingham, UK."},{"key":"S0956796813000063_ref2","first-page":"81","article-title":"Dynamic typing in polymorphic languages","volume":"5","author":"Abadi","year":"1994","journal-title":"J. Funct. Prog."},{"key":"S0956796813000063_ref28","unstructured":"van Noort T. (2012) Dynamic Typing in Type-Driven Programming, PhD thesis, Radboud University Nijmegen, Netherlands."},{"key":"S0956796813000063_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"S0956796813000063_ref12","first-page":"26","volume-title":"Proceedings of the Workshop on Types in Language Design and Implementation (TLDI '03)","author":"L\u00e4mmel","year":"2003"},{"key":"S0956796813000063_ref21","first-page":"230","volume-title":"Revised Lectures of the International School on Advanced Functional Programming, Heijen, The Netherlands","author":"Norell","year":"2008"},{"key":"S0956796813000063_ref5","first-page":"7","volume-title":"Auto-Validation d'un Syst\u00e8me de Preuves avec Familles Inductives","author":"Barras","year":"1999"},{"key":"S0956796813000063_ref3","volume-title":"Proceedings of the IFIP TC2 Working Conference on Generic Programming","author":"Altenkirch","year":"2003"},{"key":"S0956796813000063_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9075-y"},{"key":"S0956796813000063_ref11","unstructured":"Holdermans S. (in preparation) Polymorphic Dynamics for the Masses."},{"key":"S0956796813000063_ref15","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796813000063_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000848"},{"key":"S0956796813000063_ref20","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type tTheory, PhD thesis, Chalmers University of Technology, Sweden."},{"key":"S0956796813000063_ref23","volume-title":"Haskell 98 Language and Libraries: The Revised Report","author":"Peyton Jones","year":"2003"},{"key":"S0956796813000063_ref13","unstructured":"Leroy X. , Doligez D. , Frisch A. , Garrigue J. , R\u00e9my D. & Vouillon J. (2011) The OCaml System Release 3.12: Documentation and User's Manual. Tech. Report, Institut National de Recherche en Informatique et en Automatique."},{"key":"S0956796813000063_ref24","volume-title":"GADTs + Extensible Kinds = Dependent Programming","author":"Sheard","year":"2005"},{"key":"S0956796813000063_ref27","volume-title":"24th International Symposium on Implementation and Application of Functional Languages, Oxford, UK, Revised Selected Papers (IFL '12)","author":"van der Walt","year":"2012"},{"key":"S0956796813000063_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796813000063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:30Z","timestamp":1779834990000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796813000063\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,5]]}},"alternative-id":["S0956796813000063"],"URL":"https:\/\/doi.org\/10.1017\/s0956796813000063","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5]]}}}