Abstract
| 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 | |
| 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 | Poland |
| City | Warsaw, Poland |
| Period | 29/06/15 → 3/07/15 |
Fingerprint
Keywords
- units of measure
- category theory
- type theory
- dimension types
Cite this
}
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 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
ER -