@article{hamid03:safpcc,
author= {Nadeem A. Hamid and Zhong Shao and Valery Trifonov and Stefan Monnier and Zhaozhong Ni},
title= {A Syntactic Approach to Foundational Proof Carrying-Code},
journal={Journal of Automated Reasoning (Special issue on Proof-Carrying Code)},
volume={31},
number={3-4},
pages={191-229},
month=dec,
year={2003}
}
@InProceedings{hamid02:safpcc,
author = {Nadeem A. Hamid and Zhong Shao and Valery Trifonov and Stefan Monnier and Zhaozhong Ni},
title = {A Syntactic Approach to Foundational Proof-Carrying Code},
booktitle = {Proc. Seventeenth Annual IEEE Symposium on Logic In Computer Science (LICS'02)},
publisher = {IEEE},
address = {Copenhagen, Denmark},
month = {July},
year = {2002},
pages = {89-100}
}
@techreport{Monnier02,
author = "Stefan Monnier and Zhong Shao",
title = "Typed Regions",
institution = "Dept. of Computer Science, Yale University",
address = "New Haven, CT",
number = "YALEU/DCS/TR-1242",
month = oct,
year = 2002
}
@TechReport{collins02:recursive-tr,
author = {Gregory D. Collins and Zhong Shao},
title = {Intensional Analysis of Higher-Kinded Recursive Types},
institution = {Yale University},
year = {2002},
number = {YALEU/DCS/TR-1240},
month = {October}
}
@techreport{league02:piptr,
author="Christopher League and Zhong Shao and Valery Trifonov",
title="Precision in Practice: A Type-Preserving {Java} Compiler",
institution="Dept. of Computer Science, Yale University",
address="New Haven, CT", number="YALEU/DCS/TR-1223",
month=March, year=2002
}
@InProceedings{shao98:callcc,
author = {Zhong Shao and Valery Trifonov},
title = {Type-directed Continuation Allocation},
booktitle = {Second International Workshop on Types in Compilation}
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1473},
pages = {116-135},
year = 1998,
address = {Kyoto, Japan},
month = {March},
abstract = {
Suppose we translate two different source languages, $L_1$ and
$L_2$, into the same intermediate language; can they safely
interoperate in the same address space and under the same runtime
system? If $L_1$ supports first-class continuations (call/cc) and
$L_2$ does not, can $L_2$ programs call arbitrary $L_1$ functions?
Would the fact of possibly calling $L_1$ impose restrictions on the
implementation strategy of $L_2$? Can we compile $L_1$ functions
that do not invoke call/cc using more efficient techniques borrowed
from the $L_2$ implementation? Our view is that the implementation
of a common intermediate language ought to support the so-called
\emph{pay-as-you-go efficiency}: first-order monomorphic functions
should be compiled as efficiently as in C and assembly languages,
even though they may be passed to arbitrary polymorphic functions
that support advanced control primitives (e.g.~call/cc). In this
paper we present a typed intermediate language with effect and
resource annotations, ensuring the safety of inter-language calls
while allowing the compiler to choose continuation allocation
strategies.}
}
@Article{appel92:_callee_contin_passin_style,
author = {Andrew W. Appel and Zhong Shao},
title = {Callee-save registers in Continuation-Passing Style},
journal = {Lisp and Symbolic Computation},
year = 1992,
volume = 5,
number = 3,
pages = {189-219},
abstract = {Continuation-passing style (CPS) is a good abstract
representation to use for compilation and
optimization: it has a clean semantics and is easily
manipulated. We examine how CPS expresses the saving
and restoring of registers in source-language
procedure calls. In most CPS-based compilers, the
context of the calling procedure is saved in a
``continuation closure''---a single variable that is
passed as an argument to the function being
called. This closure is a record containing bindings
of all the free variables of the continuation; that
is, registers that hold values needed by the caller
``after the call'' are written to memory in the
closure, and fetched back after the call. \par
Consider the procedure-call mechanism used by
conventional compilers. In particular, registers
holding values needed after the call must be saved
and later restored. The responsibility for saving
registers can lie with the caller (a
``caller-saves'' convention) or with the called
function (``callee-saves''). In practice, to
optimize memory traffic, compilers find it useful to
have some caller-saves registers and some
callee-saves. \par ``Conventional'' CPS-based
compilers that pass a pointer to a record containing
all the variables needed after the call (i.e., the
continuation closure), are using a caller-saves
convention. We explain how te express callee-save
registers in Continuation-Passing Style, and give
measurements showing the resulting improvement in
execution time. \par }
}
@InProceedings{shao94:_space_effic_closur_repres,
author = {Zhong Shao and Andrew W. Appel},
title = {Space-Efficient Closure Representations},
booktitle = {Proc. 1994 ACM Conf. on Lisp and Functional
Programming},
pages = {150-161},
year = 1994,
address = {Orlando, FL},
month = {Jun},
abstract = {Many modern compilers implement function calls (or
returns) in two steps: first, a closure
environment is properly installed to provide access
for free variables in the target program fragment;
second, the control is transferred to the target by
a ``jump with arguments (or results.'' Closure
conversion, which decides where and how to
represent closures at runtime, is a crucial step in
compilation of functional languages. We have a new
algorithm that exploits the use of compile-time
control and data flow information to optimize
closure representations. By extensive closure
sharing and allocating as many closures in registers
as possible, our new closure conversion algorithm
reduces heap allocation by 36\% and memory fetches
for local/global variables by 43\%; and improves the
already-efficient code generated by the Standard ML
of New Jersey compiler by about 17\% on a DECstation
5000. Moreover, unlike most other approaches, our
new closure allocation scheme satisfies the strong
``safe for space complexity'' rule, thus achieving
good asymptotic space usage.}
}
@techreport{saha00:eraseitatr,
author="Bratin Saha and Valery Trifonov and Zhong Shao",
title="Fully Reflexive Intensional Type Analysis in Type Erasure Semantics",
institution="Dept. of Computer Science, Yale University",
address="New Haven, CT", number="YALEU/DCS/TR-1197",
month="June",year="2000"
}
@InProceedings{league01:_type_preser_compil_feath_java,
author = {Christopher League and Valery Trifonov and Zhong Shao},
title = {Type-Preserving Compilation of Featherweight Java},
booktitle = {Foundations of Object-Oriented Languages (FOOL8)},
year = 2001,
address = {London},
month = {January}
}
@InProceedings{yu02:bincomp,
author = {Dachuan Yu and Zhong Shao and Valery Trifonov},
title = {Supporting Binary Compatibility with Static Compilation},
booktitle = {USENIX 2nd Java[TM] Virtual Machine Research and
Technology Symposium (JVM'02)},
year = 2002,
month = {August},
abstract = {
There is an ongoing debate
in the Java community on whether statically compiled implementations
can meet the Java specification on dynamic features such as
binary compatibility.
Static compilation is sometimes desirable because it provides
better code optimization, smaller memory footprint, more robustness, and
better intellectual property protection.
Unfortunately, none of the existing static Java compilers support
binary compatibility, because it incurs unacceptable performance overhead.
In this paper, we propose a simple yet effective solution which handles
all of the binary-compatibility cases specified by the Java Language
Specification. Our experimental results using an implementation in the
GNU Java compiler
shows that the performance penalty is on average less than 2\%.
Besides solving the problem for static compilers, it's also possible to
apply the technique we used in JIT compilers to achieve an optimal
balance point between static and dynamic compilation.}
}
@InProceedings{yu02:filcomp,
author = {Dachuan Yu and Valery Trifonov and Zhong Shao},
title = {Type-Preserving Compilation of Featherweight IL},
booktitle = {Proc. 2002 Workshop on Formal Techniques for
Java-like Programs (FTfJP'02)},
year = 2002,
month = {June},
abstract = {
We present a type-preserving compilation of Featherweight IL.
Featherweight IL is a significant subset of MS IL which models
new features including value classes and their interaction with
reference classes. Our translation makes use of a high-level
intermediate language called Functional Featherweight IL.
The target language LFLINT is a low-level language which is
close to machine level implementations. During the compilation,
we preserve and further identify the basic block structures of
the program, and perform CPS and closure conversions. We use
memory based fixpoint to handle mutually recursive classes at
compile time. Standard linking techniques can be applied for
separate compilation. A type-preservation theorem for the
formal translation is presented. In the long run, our work aims
at supporting certifying compilation of high-level class-based
languages.}
}
@InProceedings{yu03:cdsa,
author = {Dachuan Yu and Nadeem A. Hamid and Zhong Shao},
title = {Building Certified Libraries for {PCC}: Dynamic Storage Allocation},
booktitle = {Proc. 2003 European Symposium on Programming (ESOP'03)},
year = 2003,
month = {April},
abstract = {
Proof-Carrying Code (PCC) allows a code producer to provide to a host
a program along with its formal safety proof. The proof attests a
certain safety policy enforced by the code, and can be mechanically
checked by the host. While this language-based approach to code
certification is very general in principle, existing PCC systems have
only focused on programs whose safety proofs can be automatically
generated. As a result, many low-level system libraries (e.g., memory
management) have not yet been handled.
In this paper, we explore a complementary approach in which general
properties and program correctness are semi-automatically certified.
In particular, we introduce a low-level language CAP for building
certified programs and present a certified library for dynamic storage
allocation.}
}
@article{yu04:cdsa-scp,
author = "Dachuan Yu and Nadeem A. Hamid and Zhong Shao",
title = "Building Certified Libraries for {PCC}: Dynamic Storage Allocation",
journal = "Science of Computer Programming",
year = "2004",
volume = "50",
number = "1-3",
pages = "101-127"
}
@InProceedings{yu04:vsca,
author = {Dachuan Yu and Zhong Shao},
title = {Verification of Safety Properties for Concurrent Assembly Code},
booktitle = {Proc. 2004 International Conference on Functional Programming (ICFP'04)},
year = 2004,
month = {September},
location = {Snowbird, Utah}
}
@TechReport{shao97:_flexib_repres_analy,
author = {Zhong Shao},
title = {Flexible Representation Analysis},
institution = {Yale University},
year = 1997,
number = {YALEU/DCS/TR-1125},
month = {April},
abstract = {Statically typed languages with Hindley-Milner
polymorphism have long been compiled using
inefficient and fully boxed data
representations. Recently, several new compilation
methods have been proposed to support more efficient
and unboxed multi-word
representations. Unfortunately, none of these
techniques is fully satisfactory. For example,
Leroy's coercion-based approach does not handle
recursive data types and mutable types well. The
type-passing approach (proposed by Harper and
Morrisett) handles all data objects, but it involves
extensive runtime type analysis and code
manipulations. \par This paper presents a new
flexible representation analysis technique that
combines the best of both approaches. Our new scheme
supports unboxed representations for recursive and
mutable types, yet it only requires little runtime
type analysis. In fact, we show that there is a
continuum of possibilities between the
coercion-based approach and the type-passing
approach. By varying the amount of boxing and the
type information passed at runtime, a compiler can
freely explore any point in the continuum--choosing
from a wide range of representation strategies based
on practical concerns. Finally, our new scheme also
easily extends to handle type abstractions across
ML-like higher-order modules. \par }
}
@InProceedings{shao97:_flexib_repres_analy,
author = {Zhong Shao},
title = {Flexible Representation Analysis},
booktitle = {Proc. 1997 {ACM} {SIGPLAN} International Conference
on Functional Programming ({ICFP}'97)},
pages = {85-98},
year = 1997,
address = {Amsterdam, The Netherlands},
month = {June},
abstract = {Statically typed languages with Hindley-Milner
polymorphism have long been compiled using
inefficient and fully boxed data
representations. Recently, several new compilation
methods have been proposed to support more efficient
and unboxed multi-word
representations. Unfortunately, none of these
techniques is fully satisfactory. For example,
Leroy's coercion-based approach does not handle
recursive data types and mutable types well. The
type-passing approach (proposed by Harper and
Morrisett) handles all data objects, but it involves
extensive runtime type analysis and code
manipulations. \par This paper presents a new
flexible representation analysis technique that
combines the best of both approaches. Our new scheme
supports unboxed representations for recursive and
mutable types, yet it only requires little runtime
type analysis. In fact, we show that there is a
continuum of possibilities between the
coercion-based approach and the type-passing
approach. By varying the amount of boxing and the
type information passed at runtime, a compiler can
freely explore any point in the continuum--choosing
from a wide range of representation strategies based
on practical concerns. Finally, our new scheme also
easily extends to handle type abstractions across
ML-like higher-order modules. \par }
}
@techreport{shao99:fullsigtr,
author="Zhong Shao",
title="Transparent Modules with Fully Syntactic Signatures (Extended Version)",
institution="Dept. of Computer Science, Yale Univ.",
address="New Haven, CT", number="YALEU/DCS/RR-1181",
month="June", year=1999
}
@inproceedings{shao99:fullsig,
author="Zhong Shao",
title="Transparent Modules with Fully Syntactic Signatures",
booktitle="Proc. 1999 ACM SIGPLAN International Conference on
Functional Programming (ICFP'99)",
pages="(to appear)",month="September",year="1999",
publisher="ACM Press"
}
@InProceedings{shao98:imp,
author = {Zhong Shao},
title = {Implementing Typed Intermediate Language},
booktitle = {Proc. 1998 {ACM} {SIGPLAN} International Conference
on Functional Programming ({ICFP}'98)},
pages = {313-323},
year = 1998,
address = {Baltimore, Maryland},
month = {September},
abstract = {}
}
@inproceedings{trifonov00:icfp,
author="Valery Trifonov and Bratin Saha and Zhong Shao",
title="Fully Reflexive Intensional Type Analysis",
booktitle="Proc. 2000 ACM SIGPLAN International Conference on
Functional Programming (ICFP'00)",
pages="(to appear)",month="September",year="2000",
publisher="ACM Press"
}
@techreport{league99:javaflint2-tr,
author="Christopher League and Zhong Shao and Valery Trifonov",
title="Representing {J}ava Classes in a Typed Intermediate Language (Extended Version)",
institution="Department of Computer Science, Yale University",
address="New Haven, CT", number="YALEU/DCS/RR-1180",
month="June", year=1999
}
@inproceedings{league99:javaflint2,
author="Christopher League and Zhong Shao and Valery Trifonov",
title="Representing {J}ava Classes in a Typed Intermediate Language",
booktitle="Proc. 1999 ACM SIGPLAN International Conference on
Functional Programming (ICFP'99)",
pages="(to appear)",month="September",year="1999",
publisher="ACM Press"
}
@TechReport{shao98:tcc-tr,
author = {Bratin Saha and Zhong Shao},
title = {Optimal Type Lifting},
institution = {Yale University},
year = 1998,
number = {YALEU/DCS/TR-1159},
month = {August},
abstract = {Modern compilers for ML-like polymorphic languages
have used explicit run-time type passing to support
advanced optimizations such as intensional type
analysis, dynamic type dispatch, and tagless garbage
collection. Unfortunately, maintaining type
information at run time can incur large overhead to
the time and space usage of a program. In this
paper, we present an optimal type-lifting algorithm
that lifts all type applications in a program to the
\emph{top} level. Our algorithm eliminates all
run-time type constructions within ane core-language
functions. In fact, it guarantees that the number of
types built at run time is strictly a compile-time
constant. We present our algorithm as a
type-preserving source-to-source transformation and
show how to extend it to handle the entire SML'97
with higher-order modules.}
}
@InProceedings{saha98:_optim_type_liftin,
author = {Bratin Saha and Zhong Shao},
title = {Optimal Type Lifting},
booktitle = {Types in Compilation Workshop},
pages = {156-177},
year = 1998,
address = {Kyoto, Japan},
month = {March},
abstract = {Modern compilers for ML-like polymorphic languages
have used explicit run-time type passing to support
advanced optimizations such as intensional type
analysis, dynamic type dispatch, and tagless garbage
collection. Unfortunately, maintaining type
information at run time can incur large overhead to
the time and space usage of a program. In this
paper, we present an optimal type-lifting algorithm
that lifts all type applications in a program to the
\emph{top} level. Our algorithm eliminates all
run-time type constructions within ane core-language
functions. In fact, it guarantees that the number of
types built at run time is strictly a compile-time
constant. We present our algorithm as a
type-preserving source-to-source transformation and
show how to extend it to handle the entire SML'97
with higher-order modules.}
}
@InProceedings{shao94:_unrol_lists,
author = {Zhong Shao and John H. Reppy and Andrew W. Appel},
title = {Unrolling Lists},
booktitle = {Proc. 1994 ACM Conf. on Lisp and Functional
Programming},
pages = {185-195},
year = 1994,
address = {Orlando, FL},
month = {Jun},
abstract = {Lists are ubiquitous in functional programs, thus
supporting lists efficiently is a major concern to
compiler writers for functional languages. Lists are
normally represented as linked \emph{cons} cells,
with each \emph{cons} cell containing a \emph{car}
(the data) and a \emph{cdr} (the link); this is
inefficient in the use of space, because 50\% of the
storage is used for links. Loops and recursions on
lists are slow on modern machines because of the
long chains of control dependences (in checking for
\emph{nil}) and data dependences (in fetching
\emph{cdr} fields). \par We present a data structure
for ``unrolled lists,'' where each cell has several
data items (\emph{car} fields) and one link
(\emph{cdr}). This reduces the memory used for
links, and it significantly shortens the length of
control-dependence and data-dependence chains in
operations on lists. \par We further present an
efficient compile-time analysis that transforms
programs written for ``ordinary'' lists into programs
on unrolled lists. The use of our new representation
requires no change to existing programs. \par We
sketch the proof of soundness of our
analysis---which is based on \emph{refinement
types}---and present some preliminary measurements
of our technique. \par }
}
@TechReport{shao98:param-tr,
author = {Zhong Shao},
title = {Parameterized Signatures and Higher-Order Modules},
institution = {Yale University},
year = 1998,
number = {YALEU/DCS/TR-1161},
month = {August},
abstract = {}
}
@InProceedings{trifonov99:resources,
author = {Valery Trifonov and Zhong Shao},
title = {Safe and Principled Language Interoperation},
booktitle = {1999 European Symposium on Programming (ESOP'99)},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
note = {To appear},
year = 1999,
address = {Amsterdam, The Netherlands},
month = {March},
abstract = {
Safety of interoperation of program fragments written in different
safe languages may fail when the languages have different systems
of computational effects: an exception raised by an ML function
may have no valid semantic interpretation in the context of a
Safe-C caller. Sandboxing costs performance and still may violate
the semantics if effects are not taken into account. We show that
effect annotations alone are insufficient to guarantee safety, and
we present a type system with bounded effect polymorphism designed
to verify the compatibility of abstract resources required by the
computational models of the interoperating languages. The type
system ensures single address space interoperability of statically
typed languages with effect mechanisms built of modules for
control and state. It is shown sound for safety with respect to
the semantics of a language with constructs for selection,
simulation, and blocking of resources, targeted as an intermediate
language for optimization of resource handling.}
}
@TechReport{shao92:_smart_recom,
author = {Zhong Shao and Andrew W. Appel},
title = {Smartest Recompilation},
institution = {Department of Computer Science, Princeton
University},
year = 1992,
number = {PU-CS-TR-395},
month = {Oct},
abstract = {To separately compile a program module in
traditional statically-typed languages, one has to
manually write down an import interface which
explicitly specifies all the external symbols
referenced in the module. Whenever the definitions
of these external symbols are changed, the module
has to be recompiled. In this paper, we present an
algorithm which can automatically infer the
``minimum'' import interface for any module in
languages based on the Damas-Milner type discipline
(e.g., ML). By ``minimum,'' we mean that the
interface specifies a set of assumptions (for
external symbols) that are just enough to make the
module type-check and compile. By compiling each
module using its ``minimum'' import interface, we
get a separate compilation method that can achieve
the following optimal property: \emph{A compilation
unit never needs to be recompiled unless its own
implementation changes.} }
}
@InProceedings{shao93:_smart_recom,
author = {Zhong Shao and Andrew W. Appel},
title = {Smartest Recompilation},
booktitle = {Proc. Twentieth ACM Symp. on Principles of
Programming Languages},
pages = {439-450},
year = 1993,
address = {Charleston, SC},
month = {Jan},
abstract = {To separately compile a program module in
traditional statically-typed languages, one has to
manually write down an import interface which
explicitly specifies all the external symbols
referenced in the module. Whenever the definitions
of these external symbols are changed, the module
has to be recompiled. In this paper, we present an
algorithm which can automatically infer the
``minimum'' import interface for any module in
languages based on the Damas-Milner type discipline
(e.g., ML). By ``minimum,'' we mean that the
interface specifies a set of assumptions (for
external symbols) that are just enough to make the
module type-check and compile. By compiling each
module using its ``minimum'' import interface, we
get a separate compilation method that can achieve
the following optimal property: \emph{A compilation
unit never needs to be recompiled unless its own
implementation changes.} }
}
@Article{appel96:_empir_analy_study_stack,
author = {Andrew W. Appel and Zhong Shao},
title = {An Empirical and Analytic Study of Stack vs. Heap
Cost for Languages with Closures},
journal = {Journal of Functional Programming},
year = 1996,
volume = 6,
number = 1,
pages = {47-74},
month = {Jan}
}
@TechReport{shao98:tcc-tr,
author = {Zhong Shao},
title = {Typed Cross-Module Compilation},
institution = {Yale University},
year = 1998,
number = {YALEU/DCS/TR-1126},
month = {June},
abstract = {}
}
@InProceedings{shao98:tcc,
author = {Zhong Shao},
title = {Typed Cross-Module Compilation},
booktitle = {Proc. 1998 {ACM} {SIGPLAN} International Conference
on Functional Programming ({ICFP}'98)},
pages = {141-152},
year = 1998,
address = {Baltimore, Maryland},
month = {September},
abstract = {}
}
@InProceedings{shao97:_typed_common_inter_format,
author = {Zhong Shao},
title = {Typed Common Intermediate Format},
booktitle = {1997 {USENIX} Conference on Domain-Specific
Languages},
year = 1997,
address = {Santa Barbara, CA},
month = {Oct},
abstract = {Application languages are very effective in solving
specific software problems. Unfortunately, they pose
great challenges to reliable and efficient
implementations. In fact, most existing application
languages are slow, interpreted, and have poor
interoperability with general-purpose languages.\par
This paper presents a framework for building a high
quality systems environment for multiple advanced
languages. Our key innovation is the use of a common
typed intermediate language, named FLINT, to model
the semantics and interactions of various
language-specific features. FLINT is based on a
predicative variant of the Girard-Reynolds
polymorphic calculus F-omega, extended with a very
rich set of primitive types and functions.\par FLINT
provides a common compiler infrastructure that can
be quickly adapted to generate compilers for new
general-purpose and domain-specific languages. With
its single unified type system, FLINT serves as a
great platform for reasoning about cross-language
inter-operations. FLINT types act as a glue to
connect language features that complicate
interoperability, such as mixed data
representations, multiple function calling
conventions, and different memory management
protocols. In addition, because all runtime
representations are determined by FLINT types,
languages compiled under FLINT can share the same
system-wide garbage collector and foreign function
call interface.\par }
}
@InProceedings{shao95:_type_compil_stand_ml,
author = {Zhong Shao and Andrew W. Appel},
title = {A Type-based Compiler for Standard ML},
booktitle = {Proc. 1995 ACM SIGPLAN Conference on Programming
Language Design and Implementation},
pages = {116-129},
year = 1995,
address = {La Jolla, CA},
month = {Jun},
abstract = {Compile-time type information should be valuable in
efficient compilation of statically typed functional
languages such as Standard ML. But how should
type-directed compilation work in real compilers,
and how much performance gain will type-based
optimizations yield? In order to support more
efficient data representations and gain more
experience about type-directed compilation, we have
implemented a new type-based middle end and back end
for the Standard ML of New Jersey compiler. We
describe the basic design of the new compiler,
identify a number of practical issues, and then
compare the performance of our new compiler with the
old non-type-based compiler. Our measurement shows
that a combination of several simple type-based
optimizations reduces heap allocation by 36\%; and
improves the already-efficient code generated by the
old non-type-based compiler by about 19\% on a
DECstation 5000.}
}
@InProceedings{shao97:_overv_flint_ml_compil,
author = {Zhong Shao},
title = {An Overview of the {FLINT/ML} Compiler},
booktitle = {Proc. 1997 {ACM} {SIGPLAN} Workshop on Types in
Compilation ({TIC}'97)},
year = 1997,
address = {Amsterdam, The Netherlands},
month = {June},
abstract = { The FLINT project at Yale aims to build a
state-of-the-art systems environment for modern
typesafe languages. One important component of the
FLINT system is a high-performance type-directed
compiler for SML'97 (extended with higher-order
modules). The FLINT/ML compiler provides several new
capabilities that are not available in other
type-based compilers: type-directed compilation is
carried over across the higher-order module
boundaries; recursive and mutable data objects can
use unboxed representations without incurring
expensive runtime cost on heavily polymorphic code;
parameterized modules (functors) can be selectively
specialized, just as normal polymorphic functions;
new type representations are used to reduce the cost
of type manipulation thus the compilation time. This
paper gives an overview of these novel aspects, and
a preliminary report on the current status of the
implementation. }
}
@techreport{saha00:itatr,
author="Bratin Saha and Valery Trifonov and Zhong Shao",
title="Fully Reflexive Intensional Type Analysis",
institution="Dept. of Computer Science, Yale University",
address="New Haven, CT", number="YALEU/DCS/TR-1194",
month="March",year="2000"
}
@techreport{monnier00:gctr,
author="Stefan Monnier and Bratin Saha and Zhong Shao",
title="Principled Scavenging",
institution="Dept. of Computer Science, Yale University",
address="New Haven, CT", number="YALEU/DCS/TR-1205",
month="November",year="2000"
}
@InProceedings{boehm93:_infer_type_maps_garbag_collec,
author = {Hans Boehm and Zhong Shao},
title = {Inferring Type Maps during Garbage Collection},
booktitle = {Proc. OOPSLA'93 Workshop on Memory Management and
Garbage Collection},
year = 1993,
address = {Washington, DC},
month = {Sept},
abstract = {Conservative garbage collectors are designed to
operate in environments that do not provide
sufficient information on the location of
pointers. Instead of relying on compiler provided
information on the location of pointers, they assume
that any bit pattern that could be a valid pointer
in fact is a valid pointer. This, however, can lead
to inefficiencies and pointer misidentifications. In
this position paper, we propose a simple runtime
method that dynamically infers the pointer layout
information during the garbage collection time. The
inferred information might be used to make the
subsequent passes of garbage collection run more
efficiently.}
}
@PhdThesis{shao94:_compil_stand_ml_effic_execut_moder_machin,
author = {Zhong Shao},
title = {Compiling Standard ML for Efficient Execution on
Modern Machines},
school = {Department of Computer Science, Princeton
University},
year = 1994,
month = {Nov}
}