Models for polymorphism over physical dimensions

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

doi:10.4230/LIPIcs.TLCA.2015.999

Models for polymorphism over physical dimensions

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

80 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 language	English
Title of host publication	13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)
Editors	Thorsten Altenkirch
Place of Publication	Wadern, Germany
Pages	999-1013
Number of pages	15
DOIs	https://doi.org/10.4230/LIPIcs.TLCA.2015.999
Publication status	Published - 2015
Event	13th International Conference on Typed Lambda Calculi and Applications TLCA15 - Warsaw, Poland, Poland Duration: 29 Jun 2015 → 3 Jul 2015

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)

Conference

Conference	13th International Conference on Typed Lambda Calculi and Applications TLCA15
Country/Territory	Poland
City	Warsaw, Poland
Period	29/06/15 → 3/07/15

Keywords

units of measure
category theory
type theory
dimension types

Access to Document

10.4230/LIPIcs.TLCA.2015.999

Atkey-etal-TLCA2015-models-polymorphism-physical-dimensionsFinal published version, 447 KBLicence: CC BY 4.0

Cite this

@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)",

note = "13th International Conference on Typed Lambda Calculi and Applications TLCA15 ; Conference date: 29-06-2015 Through 03-07-2015",

}

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 et al.
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 proceeding › Conference 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

T2 - 13th International Conference on Typed Lambda Calculi and Applications TLCA15

Y2 - 29 June 2015 through 3 July 2015

ER -

Models for polymorphism over physical dimensions

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this