Models for polymorphism over physical dimensions

Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

66 Downloads (Pure)

Abstract

We provide a categorical framework for models of a type theory that has special types for physical quantities. The types are indexed by the physical dimensions that they involve. Fibrations are used to organize this index structure in the models of the type theory. We develop some informative models of this type theory: firstly, a model based on group actions, which captures invariance under scaling, and secondly, a way of constructing new models using relational parametricity.
Original languageEnglish
Title of host publication13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)
EditorsThorsten Altenkirch
Place of PublicationWadern, Germany
Pages999-1013
Number of pages15
DOIs
Publication statusPublished - 2015
Event13th International Conference on Typed Lambda Calculi and Applications TLCA15 - Warsaw, Poland, Poland
Duration: 29 Jun 20153 Jul 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)

Conference

Conference13th International Conference on Typed Lambda Calculi and Applications TLCA15
CountryPoland
CityWarsaw, Poland
Period29/06/153/07/15

Keywords

  • units of measure
  • category theory
  • type theory
  • dimension types

Fingerprint Dive into the research topics of 'Models for polymorphism over physical dimensions'. Together they form a unique fingerprint.

  • Cite this

    Atkey, R., Ghani, N., Nordvall Forsberg, F., Revell, T., & Staton, S. (2015). Models for polymorphism over physical dimensions. In T. Altenkirch (Ed.), 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15) (pp. 999-1013). (Leibniz International Proceedings in Informatics (LIPIcs)). Wadern, Germany . https://doi.org/10.4230/LIPIcs.TLCA.2015.999