NDLI: Relational parametricity and units of measure

Please wait, while we are loading the content...

Fast and accurate flow-insensitive points-to analysis

Partitioning dataflow analyses using types

Objective ML: a simple object-oriented extension of ML

Rolling your own mutable ADT—a connection between linear types and monads

Search and imperative programming

A unified computation model for functional and logic programming

Call by need computations to root-stable form

Proof-carrying code

Does “just in time” = “better late than never”?

Parameterized types for Java

Pizza into Java: translating theory into practice

Determining the idle time of a tiling

Model checking for programming languages using VeriSoft

Synchronization transformations for parallel computing

Maximizing parallelism and minimizing synchronization with affine transforms

A Curry-Howard foundation for functional computation with control

The π-calculus in direct style

Behavioral equivalence in the polymorphic pi-calculus

Comparing the expressive power of the synchronous and the asynchronous π-calculus

Program fragments, linking, and modularization

Minimal typings in atomic subtyping

Typing algorithm in type theory with inheritance

Type checking higher-order polymorphic multi-methods

Types as abstract interpretations

Infinitary control flow analysis: a collecting semantics for closure analysis

Automatic verification of parameterized linear networks of processes

On the complexity of escape analysis

A demand-driven set-based analysis

Denotational semantics using an operationally-based term model

Constraints to stop higher-order deforestation

Reducing nondeterminism while specializing logic programs

From SOS rules to proof principles: an operational metatheory for functional languages

Relational parametricity and units of measure

High level reading and data structure compilation

PolyP—a polytypic programming language extension

First-class polymorphism with type inference

Relational parametricity and units of measure

Content Provider	ACM Digital Library
Author	Kennedy, Andrew J.
Abstract	Type systems for programming languages with numeric types can be extended to support the checking of units of measure. Quantification over units then introduces a new kind of parametric polymorphism with a corresponding Reynolds-style representation independence principle: that the behaviour of programs is invariant under changes to the units used. We prove this 'dimensional invariance' result and describe four consequences. The first is that the type of an expression can be used to derive equations which describe its properties with respect to scaling (akin to Wadler's 'theorems for free' for System F). Secondly there are certain types which are inhabited only by trivial terms. For example, we prove that a fully polymorphic square root function cannot be written using just the usual arithmetic primitives. Thirdly we exhibit interesting isomorphisms between types and for first-order types relate these to the central theorem of classical dimensional analysis. Finally we suggest that for any expression whose behaviour is dimensionally invariant there exists some equivalent expression whose type reflects this behaviour, a consequence of which would be a full abstraction result for a model of the language.
Starting Page	442
Ending Page	455
Page Count	14
File Format	PDF
ISBN	0897918533
DOI	10.1145/263699.263761
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1997-01-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in