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 | |
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 |
Keywords
- units of measure
- category theory
- type theory
- dimension types