2026-07-20T05:07:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5154 2024-03-06T10:36:09Z ddc:004 open_access

Models for Polymorphism over Physical Dimension Atkey, Robert Ghani, Neil Nordvall Forsberg, Fredrik Revell, Timothy Staton, Sam Category Theory Units of Measure Dimension Types Type Theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robert Atkey and Neil Ghani and Fredrik Nordvall Forsberg and Timothy Revell and Sam Staton 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.45 urn:nbn:de:0030-drops-51547 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.45 eng https://creativecommons.org/licenses/by/3.0/legalcode