Venue. TLCA

2015

Models for Polymorphism over Physical Dimension atkey-2015-models

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.
DOI

2014

The Structural Theory of Pure Type Systems roux-2014-the

DOI

2009

Syntax for Free: Representing Syntax with Binding Using Parametricity atkey-2009-syntax

DOI
tlca venue entries/venues/tlca.hel