NDLI: Formally optimal boxing

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

Memory subsystem performance of programs using copying garbage collection

Correctness of trap-based breakpoint implementations

Dominators, super blocks, and program coverage

The typed polymorphic label-selective λ-calculus

A functional theory of local names

From λσ to λν: a journey through calculi of explicit substitutions

Portable, unobtrusive garbage collection for multiprocessor systems

Higher-order concurrent programs with finite communication topology (extended abstract)

Proving concurrent constraint programs correct

Manifest types, modules, and separate compilation

A type-theoretic approach to higher-order modules with sharing

A type system for prototyping languages

Decidable bounded quantification

Soft typing with conditional types

Automated synthesis of interface adapters for reusable classes

Implementation of the typed call-by-value λ-calculus using a stack of regions

Deriving algorithms from type inference systems: application to strictness analysis

Formally optimal boxing

Combinations of abstract domains for logic programming

Analyzing logic programs with dynamic scheduling

Higher-order equational logic programming

A needed narrowing strategy

Detecting pipeline structural hazards quickly

An incremental algorithm for maintaining the dominator tree of a reducible flowgraph

Value dependence graphs: representation without taxation

Lazy array data-flow dependence analysis

An operational framework for value-passing processes

CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms (preliminary report)

Combinatory representation of mobile processes

Multi-pass execution of functional logic programs

Composing tree attributions

A staging calculus and its application to the verification of translators (preliminary report)

Reducing indirect function call overhead in C++ programs

Call forwarding: a simple interprocedural optimization technique for dynamically typed languages

The revival transformation

Selective and lightweight closure conversion

Representing monads

A generic account of continuation-passing styles

Building interpreters by composing monads

Formally optimal boxing

Content Provider	ACM Digital Library
Author	Henglein, Fritz Jørgensen, Jesper
Abstract	An important implementation decision in polymorphically typed functional programming language is whether to represent data in boxed or unboxed form and when to transform them from one representation to the other. Using a language with explicit representation types and boxing/unboxing operations we axiomatize equationally the set of all explicitly boxed versions, called completions, of a given source program. In a two-stage process we give some of the equations a rewriting interpretation that captures eliminating boxing/unboxing operations without relying on a specific implementation or even semantics of the underlying language. The resulting reduction systems operate on congruence classes of completions defined by the remaining equations E, which can be understood as moving boxing/unboxing operations along data flow paths in the source program. We call a completion eopt formally optimal if every other completion for the same program (and at the same representation type) reduces to eopt under this two-stage reduction.We show that every source program has formally optimal completions, which are unique modulo E. This is accomplished by first “polarizing” the equations in E and orienting them to obtain two canonical (confluent and strongly normalizing) rewriting systems. The completions produced by Leroy's and Poulsen's algorithms are generally not formally optimal in our sense.The rewriting systems have been implemented and applied to some simple Standard ML programs. Our results show that the amount of boxing and unboxing operations is also in practice substantially reduced in comparison to Leroy's completions. This analysis is intended to be integrated into Tofte's region-based implementation of Standard ML currently underway at DIKU.
Starting Page	213
Ending Page	226
Page Count	14
File Format	PDF
ISBN	0897916360
DOI	10.1145/174675.177874
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1994-02-01
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Type inference Representation analysis Polymorphism
Content Type	Text
Resource Type	Article

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

J.Palsberg. Optimal representation of polymorphic types with subtyping (1996)

Optimal Representations of Polymorphic Types with Subtyping

Optimal Representations of Polymorphic Types with Subtyping (Extended Abstract) (1997)

Optimal Representations of Polymorphic Types with Subtyping (1996)

Optimal Representations of Polymorphic Types with Subtyping (1996)

Polymorphism, subtyping, and type inference in MLsub

Formally optimal boxing

Optimal inference of fields in row-polymorphic records

HMF: simple type inference for first-class polymorphism

Formally optimal boxing

Similar Documents

J.Palsberg. Optimal representation of polymorphic types with subtyping (1996)

Optimal Representations of Polymorphic Types with Subtyping

Optimal Representations of Polymorphic Types with Subtyping (Extended Abstract) (1997)

Optimal Representations of Polymorphic Types with Subtyping (1996)

Optimal Representations of Polymorphic Types with Subtyping (1996)

Polymorphism, subtyping, and type inference in MLsub

Formally optimal boxing

Optimal inference of fields in row-polymorphic records

HMF: simple type inference for first-class polymorphism

Formally optimal boxing