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

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.
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

Fingerprint

Type Theory
Polymorphism
Relational Model
Fibration
Group Action
Categorical
Invariance
Model
Scaling
Model-based

Keywords

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

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
Atkey, Robert ; Ghani, Neil ; Nordvall Forsberg, Fredrik ; Revell, Timothy ; Staton, Sam. / Models for polymorphism over physical dimensions. 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). editor / Thorsten Altenkirch. Wadern, Germany , 2015. pp. 999-1013 (Leibniz International Proceedings in Informatics (LIPIcs)).
@inproceedings{9af450312b474e57956a4d51eae72d13,
title = "Models for polymorphism over physical dimensions",
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.",
keywords = "units of measure, category theory, type theory, dimension types",
author = "Robert Atkey and Neil Ghani and {Nordvall Forsberg}, Fredrik and Timothy Revell and Sam Staton",
year = "2015",
doi = "10.4230/LIPIcs.TLCA.2015.999",
language = "English",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
pages = "999--1013",
editor = "Thorsten Altenkirch",
booktitle = "13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)",

}

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). Leibniz International Proceedings in Informatics (LIPIcs), Wadern, Germany , pp. 999-1013, 13th International Conference on Typed Lambda Calculi and Applications TLCA15, Warsaw, Poland, Poland, 29/06/15. https://doi.org/10.4230/LIPIcs.TLCA.2015.999

Models for polymorphism over physical dimensions. / Atkey, Robert; Ghani, Neil; Nordvall Forsberg, Fredrik; Revell, Timothy; Staton, Sam.

13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). ed. / Thorsten Altenkirch. Wadern, Germany , 2015. p. 999-1013 (Leibniz International Proceedings in Informatics (LIPIcs)).

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

TY - GEN

T1 - Models for polymorphism over physical dimensions

AU - Atkey, Robert

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Revell, Timothy

AU - Staton, Sam

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - units of measure

KW - category theory

KW - type theory

KW - dimension types

UR - http://www.mimuw.edu.pl/tlca/

U2 - 10.4230/LIPIcs.TLCA.2015.999

DO - 10.4230/LIPIcs.TLCA.2015.999

M3 - Conference contribution book

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 999

EP - 1013

BT - 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)

A2 - Altenkirch, Thorsten

CY - Wadern, Germany

ER -

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