Skip to main content
SpringerLink
Log in

Types for Units-of-Measure: Theory and Practice

  • Chapter
Central European Functional Programming School (CEFP 2009)

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

Included in the following conference series:

Abstract

Units-of-measure are to science what types are to programming. In science and engineering, dimensional and unit consistency provides a first check on the correctness of an equation or formula, just as in programming the validation of a program by the type-checker eliminates one possible reason for failure.

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. The International System of Units (SI). Technical report, Bureau International des Poids et Mesures (2006)

    Google Scholar 

  2. Allen, E., Chase, D., Hallett, J., Lunchangco, V., Maessen, J.-W., Ryu, S., Steele Jr., G.L., Tobin-Hochstadt, S.: The Fortress Language Specification, Version 1.0 (2008)

    Google Scholar 

  3. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1988)

    MATH  Google Scholar 

  4. Bird, R.S., Paterson, R.: de brujn notation as a nested datatype. Journal of Functional Programming 9(1), 77–92 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  5. Birkhoff, G.: Hydrodynamics: A Study in Logic, Fact and Similitude. Princeton University Press, Princeton (1960)

    MATH  Google Scholar 

  6. Buckwalter, B.: dimensional: statically checked physical dimensions for Haskell (2008)

    Google Scholar 

  7. Kennedy, A.J.: Programming Languages and Dimensions. PhD thesis, University of Cambridge (1995)

    Google Scholar 

  8. Kennedy, A.J.: Type inference and equational theories. Technical Report LIX/RR/96/09, École Polytechnique, Paris, France (1996)

    Google Scholar 

  9. Kennedy, A.J.: Relational parametricity and units of measure. In: POPL 1997: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 442–455. ACM Press, New York (1997)

    Google Scholar 

  10. Kennedy, A.J.: Formalizing an extensional semantics for units of measure. In: 3rd ACM SIGPLAN Workshop on Mechanizing Metatheory, WMM (2008)

    Google Scholar 

  11. Le Botlan, D., Rémy, D.: MLF: Raising ML to the power of System F. In: 8th ACM SIGPLAN International Conference on Functional Programming, ICFP (2003)

    Google Scholar 

  12. Leijen, D.: HMF: Simple type inference for first-class polymorphism. In: 13th ACM SIGPLAN International Conference on Functional Programming, ICFP (2008)

    Google Scholar 

  13. Lindley, S.: Many holes in Hindley-Milner. In: Proceedings of the 2008 Workshop on ML (2008)

    Google Scholar 

  14. Milner, R.: A theory of type polymorphism in programming. Journal of computer and system sciences 17, 348–375 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  15. NASA. Mars Climate Orbiter Mishap Investigation Board: Phase I Report, (November 1999)

    Google Scholar 

  16. Pierce, B.C. (ed.): Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  17. Pierce, B.C. (ed.): Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)

    MATH  Google Scholar 

  18. Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes: The Art of Scientific Computing, 3rd edn. Cambridge University Press, Cambridge (2007)

    MATH  Google Scholar 

  19. Schabel, M.C., Watanabe, S.: Boost.Units (2008)

    Google Scholar 

  20. Schrijvers, T., Peyton Jones, S., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for GADTs. In: International Conference on Functional Programming, ICFP (2009)

    Google Scholar 

  21. Szirtes, T.: Applied Dimensional Analysis and Modeling, 2nd edn. Butterworth-Heinemann, Butterworths (2007)

    MATH  Google Scholar 

  22. Vytiniotis, D., Peyton Jones, S., Schrijvers, T.: let should not be generalized. In: Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI (2010)

    Google Scholar 

  23. Vytiniotis, D., Weirich, S., Peyton Jones, S.: FPH: First-class polymorphism for Haskell. In: 13th ACM SIGPLAN International Conference on Functional Programming, ICFP (2008)

    Google Scholar 

  24. Wadler, P.: Theorems for free! In: Proceedings of the 4th International Symposium on Functional Programming Languages and Computer Architecture (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Andrew Kennedy

Authors
  1. Andrew Kennedy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Department of Programming Languages and Compilers, Eötvös Loránd University, Pázmány Péter Sétány 1/C, 1117, Budapest, Hungary

    Zoltán Horváth  & Viktória Zsók  & 

  2. Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500, Nijmegen, GL, The Netherlands

    Rinus Plasmeijer

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Kennedy, A. (2010). Types for Units-of-Measure: Theory and Practice. In: Horváth, Z., Plasmeijer, R., Zsók, V. (eds) Central European Functional Programming School. CEFP 2009. Lecture Notes in Computer Science, vol 6299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17685-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17685-2_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17684-5

  • Online ISBN: 978-3-642-17685-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation