Models for polymorphism over physical dimensions

Atkey, Robert and Ghani, Neil and Nordvall Forsberg, Fredrik and Revell, Timothy and Staton, Sam; Altenkirch, Thorsten, ed. (2015) Models for polymorphism over physical dimensions. In: 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Leibniz International Proceedings in Informatics (LIPIcs) . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, POL, pp. 999-1013. (https://doi.org/10.4230/LIPIcs.TLCA.2015.999)

[thumbnail of Atkey-etal-TLCA2015-models-polymorphism-physical-dimensions]
Preview
 Text. Filename: Atkey_etal_TLCA2015_models_polymorphism_physical_dimensions.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (457kB)| Preview

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.

ORCID iDs

Atkey, Robert ORCID logoORCID: https://orcid.org/0000-0002-4414-5047, Ghani, Neil ORCID logoORCID: https://orcid.org/0000-0002-3988-2560, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288, Revell, Timothy and Staton, Sam; Altenkirch, Thorsten
CORE (COnnecting REpositories)