No CrossRef data available.
Article contents
A library for polymorphic dynamic typing
Part of:
JFP Research Articles
Published online by Cambridge University Press: 22 October 2013
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
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 polymorphic type to be instantiated to a less general (possibly monomorphic) type without compromising type soundness.
Information
- Type
- Articles
- Information
- Copyright
- Copyright © Cambridge University Press 2013
References
Abadi, M., Cardelli, L., Pierce, B. & Plotkin, G. (1991) Dynamic typing in a statically typed language. ACM Trans. Prog. Lang. Syst. 13 (2), 237–268.CrossRefGoogle Scholar
Abadi, M., Cardelli, L., Pierce, B., Rémy, D. & Taylor, R. (1994) Dynamic typing in polymorphic languages. J. Funct. Prog. 5 (1), 81–110.Google Scholar
Altenkirch, T. & McBride, C. (2003) Generic programming within dependently typed programming. Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schloss Dagstuhl, Germany, July 2002.Google Scholar
Baars, A. & Swierstra, D. (2002) Typing dynamic typing. Proceedings of the International Conference on Functional Programming (ICFP '02). Pittsburgh, PA, USA.Google Scholar
Barras, B. (1999, Nov) Auto-Validation d'un Système de Preuves avec Familles Inductives, Thèse de doctorat, Université Paris 7.Google Scholar
Brady, E. (2011) Epic – a library for generating compilers. In Proceedings of the 12th International Conference on Trends in Functional Programming (TFP '11). New York: Springer-Verlag.Google Scholar
Chapman, J. (2008) Type Checking and Normalisation, PhD thesis, University of Nottingham, Nottingham, UK.Google Scholar
Chapman, J., Dagand, P.-É., McBride, C. & Morris, P. (2010) The gentle art of levitation. Proceedings of the 15th ACM Sigplan International Conference on Functional Programming (ICFP '10), Baltimore, MD, September 27–29, 2010.Google Scholar
Cheney, J. & Hinze, R. (2002) A lightweight implementation of generics and dynamics. Proceedings of the Haskell Workshop (Haskell '02), Pittsburgh, PA, USA.Google Scholar
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).Google Scholar
Holdermans, S. (in preparation) Polymorphic Dynamics for the Masses.Google Scholar
Lämmel, R. & PeytonJones, S. Jones, S. (2003) Scrap your boilerplate: A practical design pattern for generic programming. In Proceedings of the Workshop on Types in Language Design and Implementation (TLDI '03), New Orleans, LA, pp. 26–37.Google Scholar
Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, 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.Google Scholar
McBride, C. (2003) First-order unification by structural recursion. J. Funct. Prog. 13 (6), 1061–1075.CrossRefGoogle Scholar
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).CrossRefGoogle Scholar
McBride, C. & McKinna, J. (2004) The view from the left. J. Funct. Prog 14 (1), 69–111.CrossRefGoogle Scholar
McBride, C. & Paterson, R. (2008) Applicative programming with effects. J. Funct. Prog. 18 (1), 1–13.CrossRefGoogle Scholar
Norell, U. (2007) Towards a Practical Programming Language Based on Dependent Type tTheory, PhD thesis, Chalmers University of Technology, Sweden.Google Scholar
Norell, U. (2008) Dependently typed programming in Agda. In Revised Lectures of the International School on Advanced Functional Programming, Heijen, The Netherlands, Lecture Notes in Computer Science, vol. 5832, Koopman, Pieter, Plasmeijer, Rinus & Swierstra, Doaitse (eds). New York, NY: Springer-Verlag. pp. 230–266.Google Scholar
Oury, N. & Swierstra, W. (2008) The power of Pi. Proceedings of the International Conference on Functional Programming (ICFP '08), Victoria, BC, Canada.Google Scholar
Peyton Jones, S. (ed). (2003) Haskell 98 Language and Libraries: The Revised Report. Cambridge, UK: Cambridge University Press.Google Scholar
Sheard, T., Hook, J. & Linger, N. (2005) GADTs + Extensible Kinds = Dependent Programming. Techical Report, Portland State University, Portland, OR.Google Scholar
Sheard, T. & Pasǎlić, E. (2008) Meta-programming with built-in type equality. Electron. Notes Theor. Comput. Sci. 199, 49–65.CrossRefGoogle Scholar
Swierstra, W. (2010) More dependent types for distributed arrays. Higher Order Symb. Comput. 23 (4), 489–506.CrossRefGoogle Scholar
van der Walt, P & Swierstra, W. (2012) Engineering proof by reflection in Agda. In 24th International Symposium on Implementation and Application of Functional Languages, Oxford, UK, Revised Selected Papers (IFL '12). Oxford, UK: Department of Computer Science, University of Oxford.Google Scholar
van Noort, T. (2012) Dynamic Typing in Type-Driven Programming, PhD thesis, Radboud University Nijmegen, Netherlands.Google Scholar
You have
Access
- 1
- Cited by
Discussions
No Discussions have been published for this article.