Picture of sea vessel plough through rough maritime conditions

Innovations in marine technology, pioneered through Open Access research...

Strathprints makes available scholarly Open Access content by researchers in the Department of Naval Architecture, Ocean & Marine Engineering based within the Faculty of Engineering.

Research here explores the potential of marine renewables, such as offshore wind, current and wave energy devices to promote the delivery of diverse energy sources. Expertise in offshore hydrodynamics in offshore structures also informs innovations within the oil and gas industries. But as a world-leading centre of marine technology, the Department is recognised as the leading authority in all areas related to maritime safety, such as resilience engineering, collision avoidance and risk-based ship design. Techniques to support sustainability vessel life cycle management is a key research focus.

Explore the Open Access research of the Department of Naval Architecture, Ocean & Marine Engineering. Or explore all of Strathclyde's Open Access research...

Abstraction and invariance for algebraically indexed types

Atkey, Robert and Johann, Patricia and Kennedy, Andrew (2013) Abstraction and invariance for algebraically indexed types. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM Press, pp. 87-100. ISBN 978-1-4503-1832-7

[img]
Preview
PDF
popl13.pdf
Preprint

Download (477kB) | Preview

Abstract

Reynolds’ relational parametricity provides a powerful way to rea- son about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ the- ory exists, exploiting invariance to yield “free theorems”, non- inhabitation results, and encodings of algebraic datatypes. Outside computer science, invariance is a common theme running through many areas of mathematics and physics. For example, the area of a triangle is unaltered by rotation or flipping. If we scale a trian- gle, then we scale its area, maintaining an invariant relationship be- tween the two. The transformations under which properties are in- variant are often organised into groups, with the algebraic structure reflecting the composability and invertibility of transformations. In this paper, we investigate programming languages whose types are indexed by algebraic structures such as groups of ge- ometric transformations. Other examples include types indexed by principals–for information flow security–and types indexed by distances–for analysis of analytic uniform continuity properties. Following Reynolds, we prove a general Abstraction Theorem that covers all these instances. Consequences of our Abstraction Theo- rem include free theorems expressing invariance properties of pro- grams, type isomorphisms based on invariance properties, and non- definability results indicating when certain algebraically indexed types are uninhabited or only inhabited by trivial programs. We have fully formalised our framework and most examples in Coq.