Skip to main content
SpringerLink
Log in

Generic Programming in Ωmega

  • Conference paper
Datatype-Generic Programming (SSDGP 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4719))

Included in the following conference series:

Abstract

“Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of abstraction; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms.”

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Antoy, S.: Definitional trees. In: Kirchner, H., Levi, G. (eds.) Algebraic and Logic Programming. LNCS, vol. 632, pp. 143–157. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  2. Augustsson, L.: Cayenne – a language with dependent types. ACM SIGPLAN Notices 34(1), 239–250 (1999)

    Article  Google Scholar 

  3. Augustsson, L.: Equality proofs in Cayenne (July 11, 2000), http://www.cs.chalmers.se /~augustss/cayenne/eqproof.ps

  4. Cardelli, L., Wegner, P.: On understanding types, data abstraction and polymorphism. ACM Computing Surveys 17(4), 471–522 (1985)

    Article  Google Scholar 

  5. Chen, C., Xi, H.: Combining programming with theorem proving. In: ICFP 2005 (2005), http://www.cs.bu.edu /~hwxi/

  6. Coquand, C.: Agda is a system for incrementally developing proofs and programs. Web page describing AGDA: http://www.cs.chalmers.se /~catarina/agda/

  7. Coquand, T., Dybjer, P.: Inductive definitions and type theory: an introduction (preliminary version). In: Thiagarajan, P.S. (ed.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 880, pp. 60–76. Springer, Heidelberg (1994)

    Google Scholar 

  8. Davies, R.: A refinement-type checker for Standard ML. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  9. Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Fridlender, D., Indrika, M.: Do we need dependent types? J. Funct. Program 10(4), 409–415 (2000)

    Article  MATH  Google Scholar 

  11. Luo, Z., Pollack, R.: LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, Updated version (May 1992)

    Google Scholar 

  12. McBride, C.: Epigram: Practical programming with dependent types. In: Notes from the 5th International Summer School on Advanced Functional Programming (August 2004)Available at: http://www.dur.ac.uk /CARG/epigram/epigram-afpnotes.pdf

  13. Nordstrom, B.: The ALF proof editor (March 20, 1996), ftp://ftp.cs.chalmers.se /pub/users/ilya/FMC/alfintro.ps.gz

  14. Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science. Logic and Computer Science, pp. 361–386. Academic Press, London (1990)

    Google Scholar 

  15. Jones, S.P.: Special issue: Haskell 98 language and libraries. Journal of Functional Programming 13 (January 2003)

    Google Scholar 

  16. Pfenning, F., Schürmann, C.: System description: Twelf — A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated Deduction - CADE-16. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A type system for certified binaries. ACM SIGPLAN Notices 37(1), 217–232 (2002)

    Article  MATH  Google Scholar 

  18. Sheard, T.: Using MetaML: A staged programming language. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol. 1608, pp. 207–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Sheard, T., Peyton-Jones, S.: Template meta-programming for Haskell. In: Proc. of the workshop on Haskell, pp. 1–16. ACM Press, New York (2002)

    Google Scholar 

  20. Stone, C.A., Harper, R.: Deciding type equivalence in a language with singleton kinds. In: Conference Record of POPL 2000: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, pp. 214–227 (2000)

    Google Scholar 

  21. Stump, A.: Imperative LF meta-programming. In: Logical Frameworks and Meta-Languages workshop (July 2004), Available at: http://cs-www.cs.yale.edu/homes/carsten/lfm04/

  22. Taha, W., Sheard, T.: MetaML: Multi-stage programming with explicit annotations. Theoretical Computer Science 248(1-2) (2000)

    Google Scholar 

  23. The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 7.4. INRIA (2003), http://pauillac.inria.fr/coq/doc/main.html

  24. Westbrook, E., Stump, A., Wehrman, I.: A language-based approach to functionally correct inperative programming. Technical report, Washington University in St. Louis, (2005), Available at: http://cl.cse.wustl.edu/

  25. Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University (1997)

    Google Scholar 

  26. Xi, H.: Applied type systems. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 394–408. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  27. Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. ACM SIGPLAN Notices 33(5), 249–257 (1998)

    Article  Google Scholar 

  28. Xi, H., Pfenning, F.: Dependent types in practical programming. In: ACM (ed.) POPL 1999. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, ACM SIGPLAN Notices, January 20-22, 1999, pp. 214–227. ACM Press, New York (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Maseeh College of Engineering and Computer Science, Portland State University, USA

    Tim Sheard

Authors
  1. Tim Sheard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Roland Backhouse Jeremy Gibbons Ralf Hinze Johan Jeuring

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sheard, T. (2007). Generic Programming in Ωmega. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds) Datatype-Generic Programming. SSDGP 2006. Lecture Notes in Computer Science, vol 4719. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76786-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-76786-2_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-76785-5

  • Online ISBN: 978-3-540-76786-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation