From system F to typed assembly language
Published 1 January 1998Open access
Greg Morrisett, David Walker, Karl Crary, Neal Glew
Citations282
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The TAL presented is based on a conventional RISC assembly language, but its static type system provides support for enforcing high-level language abstractions, such as closures, tuples, and objects, as well as user-defined abstract data types.
Abstract
We motivate the design of a statically typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static type system provides support for enforcing high-level language abstractions, such as closures, tuples, and objects, as well as user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the typing constructs place almost no restrictions on low-level optimizations such as register allocation, instruction selection, or instruction scheduling.Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly language provide a fully automatic way to produce proof carrying code, suitable for use in systems where untrusted and potentially malicious code must be checked for safety before execution.
Keywords
Computer Science
Theoretical Computer ScienceLinear logic
4,030 Citations1987Jean-Yves Girard
Material for the course Lineare Logik mit Anwendungen, Technische Hochschule Darmstadt, Sommersemester 1996 is reprinted here in rough draft form.
The MIT Press eBooksThe Definition of Standard ML
2,411 Citations1997Robin Milner, Robert Harper +2 more
This book provides a formal definition of Standard ML for the benefit of all concerned with the language, including users and implementers, and the authors have defined their semantic objects in mathematical notation that is completely independent of StandardML.
Addison-Wesley Longman Publishing Co., Inc. eBooksThe Java Virtual Machine Specification
2,047 Citations1996Tim Lindholm, Frank Yellin
This second edition specifies the newest version of the Java virtual machine and provides a fascinating view into the inner workings of theJava 2 platform.
Proof-carrying code
1,807 Citations1997George C. Necula
It is shown in this paper how proof-carrying code might be used to develop safe assembly-language extensions of ML programs and the adequacy of concrete representations for the safety policy, the safety proofs, and the proof validation is proved.
Efficient software-based fault isolation
1,217 Citations1993Robert Wahbe, Steven Lucco +2 more
It is demonstrated that for frequently communicating modules, implementing fault isolation in software rather than hardware can substantially improve end-to-end application performance.
Theoretical Computer ScienceCall-by-name, call-by-value and the λ-calculus
1,158 Citations1975Gordon Plotkin
This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call- by-name, and finds that operational equality is not preserved by either of the simulations.
The Definition of Standard ML (Revised)
983 Citations1997Robin Milner, Robert Harper +2 more
Part 1 Syntax of the core: reserved words special constants comments identifiers lexical analysis infixed operators derived forms grammar syntactic restrictions.
Extensibility safety and performance in the SPIN operating system
955 Citations1995Brian N. Bershad, Stefan Savage +6 more
This paper describes the motivation, architecture and performance of SPIN, an extensible operating system that provides an extension infrastructure together with a core set of extensible services that allow applications to safely change the operating system's interface and implementation.
The Computer JournalThe Mechanical Evaluation of Expressions
932 Citations1964P. J. Landin
It is shown how some forms of expression in current programming languages can be modelled in Church's X-notation, and a way of "interpreting" such expressions is described, which suggests a method of analyzing the things computer users write.
Lecture notes in computer scienceTowards a theory of type structure
813 Citations1974John Reynolds
It can be shown that B maps every type expression into a functor from C T into C, that w = w' implies w[w] = B[w'], and that B[WlI: 2](~) = B [Wl][ D I t I B[ w2](D) ]
Software Practice and ExperienceGarbage collection in an uncooperative environment
630 Citations1988Hans‐Juergen Boehm, Mark Weiser
This approach greatly simplifies the implementation of languages supporting garbage collection and allows conventional compilers to be used with a garbage collector, either as the primary means of storage reclamation, or as a debugging tool.
Dependent types in practical programming
576 Citations1999Hongwei Xi, Frank Pfenning
An approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema, which allows specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization.
Safe kernel extensions without run-time checking
502 Citations1996George C. Necula, Peter Lee
PCC binaries can be executed with no run-time over-head, beyond a one-time cost of 1 to 3 milliseconds for validating the enclosed proofs, and are formally guaranteed to be safe and are faster than packet filters created using Berkeley Packet Filters, Software Fault Isolation, or safe languages such as Modula-3.
Studies in logic and the foundations of mathematicsUne Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des Types
447 Citations1971
ACM Transactions on Programming Languages and SystemsAbstract types have existential type
432 Citations1988John C. Mitchell, Gordon Plotkin
This work uses a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls.
DSpace@MIT (Massachusetts Institute of Technology)Rabbit: A Compiler for Scheme
402 Citations1978Jr. Guy L. Steele
A compiler for the lexically-scoped dialect of LISP known as SCHEME, which handles only a small basis set which reflects the semantics of lambda-calculus, and serves to produce code as good as that produced by more traditional compilers.
Linear Types can Change the World
387 Citations1990Philip Wadler
Linear types extend Schmidt's notion of single threading; provide an alternative to Hudak and Bloss' update analysis; and provide a practical complement to Lafont and Holmstrr om's elegant linear languages.
Mathematical Structures in Computer ScienceRepresenting Control: a Study of the CPS Transformation
352 Citations1992Oliver Danvy, Andrzex Filinski
It is shown that by appropriate η-expansion of Fisher and Plotkin's two-pass equational specification of the CPS transform, a static and context-free separation of the result terms into “essential” and “administrative” constructs can be obtained, leading to a simple and efficient one-pass transformation algorithm.
TIL
316 Citations1996David Tarditi, Greg Morrisett +4 more
TIL introduced and popularized the notion of a certifying compiler, which attaches a checkable certificate of safety to its generated code, inspiring the development of Proof-Carrying Code and Typed Assembly Language as certified object code formats.
Eliminating array bound checking through dependent types
287 Citations1998Hongwei Xi, Frank Pfenning
A type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice.
ACM SIGPLAN NoticesOrbit
259 Citations2004David Kranz, Richard Kelsey +4 more
Orbit was an optimizing compiler for T, a dialect of Scheme, that directly spawned six PhD theses and one Masters thesis, and influenced many other projects as well, including SML of New Jersey.
Lecture notes in computer scienceStandard ML of New Jersey
245 Citations1991Andrew W. Appel, David MacQueen
The Standard ML of New Jersey compiler has been under development for five years now and has developed a robust and complete environment that supports the implementation of large software systems and generates efficient code.
Unboxed objects and polymorphic typing
220 Citations1992Xavier Leroy
A program transformation that allows languages with polymorphic typing to be implemented with unboxed, multi-word data representations with coercions between various representations, based on a typing derivation is presented.
Typed closure conversion
208 Citations1996Yasuhiko Minamide, Greg Morrisett +1 more
This work presents closure conversion as a type-directed, and type-preserving translation for both the simply-typed and the polymorphic ¿-calculus, and exploits a variant of the Harper-Lillibridge "translucent type" formalism to characterize the types of polymorphic closures.
LISP and Symbolic ComputationSimple imperative polymorphism
193 Citations1995Andrew K. Wright
A study of a number of ML programs shows that the inability to type all Hindley-Milner typable expressions seldom impacts realistic programs, so with a module system that separates specifications from implementations, imperative features can be freely used to implement polymorphic specifications.
The Glasgow Haskell Compiler: a technical overview
191 Citations1993SL Peyton Jones, Kevin Hammond +4 more
An overview of the Glasgow Haskell compiler is given, focusing especially on way in which the compiler has been able to exploit the rich theory of functional languages to give very practical improvements in the compiler.
Information and ComputationType inference for polymorphic references
186 Citations1990Mads Tofte
A modified type inference system is presented and it is proved its soundness using operational semantics that it is decidable whether, given an expression e, any type can be inferred for e.
LISP and Symbolic ComputationState in Haskell
186 Citations1995John Launchbury, Simon Jones
This work presents a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language.
TALx86: A Realistic Typed Assembly Language∗
184 Citations1999Greg Morrisett, Karl Crary +7 more
The goal of typed assembly language (TAL) is to provide a low-level, statically typed target language that is better suited than Java bytecodes for supporting a wide variety of source languages and a number of important optimizations.
Information and ComputationInheritance as implicit coercion
179 Citations1991Val Breazu-Tannen, Thierry Coquand +2 more
A method for providing semantic interpretations for languages with a type system featuring inheritance polymorphism, illustrated on an extension of the language Fun of Cardelli and Wegner, which is interpreted via a translation into an extended polymorphic lambda calculus.
Compiling with proofs
169 Citations1998George C. Necula, Peter Lee
This dissertation shows how standard decision procedures can be adapted so that they can produce detailed proofs of the proved predicates and also how these proofs can be encoded compactly and checked efficiently.
Continuation-passing, closure-passing style
168 Citations1989Andrew W. Appel, Trevor Jim
This work implemented a continuation-passing style (CPS) code generator for ML that separates the code generation into phases that rewrite this representation of the language into ever-simpler forms.
Lambda calculus schemata
136 Citations1972Michael J. Fischer
A lambda-calculus schema is an expression of the lambda calculus augmented by uninterpreted constant and operator symbols that is an abstraction of programming languages such as LISP which permit functions to be passed to and returned from other functions.
From region inference to von Neumann machines via region representation inference
134 Citations1996Lars Birkedal, Mads Tofte +1 more
This paper is concerned with mapping the mathematical model of region inference onto real machines by composing region inference with Region Representation Inference, which gradually refines region information till it is directly implementable on conventional von Neumann machines.
Abstract models of memory management
127 Citations1995Greg Morrisett, Matthias Felleisen +1 more
A series of calculi are developed that are just low-level enough that they can express allocation and garbage collection, yet are sufficiently abstract that they may formally prove the correctness of various memory management strategies.
Intensional polymorphism in type-erasure semantics
119 Citations1998Karl Crary, Stephanie Weirich +1 more
This work presents a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing, and allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.
ACM SIGPLAN NoticesORBIT: an optimizing compiler for scheme
114 Citations1986Norman I. Adams, David Kranz +4 more
Flexible type analysis
101 Citations1999Karl Crary, Stephanie Weirich
The language LX is presented, which provides a rich language of type constructors supporting type analysis (possibly of previous-stage types) as a programming idiom, and is quite flexible, supporting a variety of other applications such as analysis of quantified types, analysis with incomplete type information, and type classes.
Compiling with Types
92 Citations1995Greg Morrisett
This thesis provides a general framework, called type-directed compilation, that allows compiler writers to take advantage of types at all stages in compilation, and builds a new compiler for SML called TIL that eliminates most restrictions on the representations of values.
Lecture notes in computer scienceA taste of linear logic
83 Citations1993Philip Wadler
This tutorial paper provides an introduction to intuitionistic logic and linear logic, and shows how they correspond to type systems for functional languages via the notion of ‘Propositions as Types’.
Type-safe linking and modular assembly language
81 Citations1999Neal Glew, Greg Morrisett
This work presents a formal model of typed object files and a set of inference rules that are sufficient to guarantee that type safety is preserved by the linking process.
ACM SIGOPS Operating Systems ReviewExtensibility safety and performance in the SPIN operating system
76 Citations1995Brian N. Bershad, Stefan Savage +6 more
Lecture notes in computer scienceStack-based Typed Assembly Language
72 Citations1998Greg Morrisett, Karl Crary +2 more
Explicit polymorphism and CPS conversion
71 Citations1993Robert Harper, Mark Lillibridge
The typing properties of CPS conversion for an extension of Fω with control operators is studied, finding results similar to those obtained for the call-by value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values.
Flexible representation analysis
71 Citations1997Zhong Shao
This paper presents a new flexible representation analysis technique that combines the best of both approaches, and shows that there is a continuum of possibilities between the coercion-based approach and the type-passing approach.
Tag-free garbage collection using explicit type parameters
67 Citations1994Andrew Tolmach
A practical tag-free garbage collector based on explicit type parameterization of polymorphic functions, for a dialect of ML, and preliminary performance measurements suggest that the overhead of passing type information explicitly can be made acceptably small.
Lecture notes in computer scienceCorrectness of procedure representations in higher-order assembly language
51 Citations1992Mitchell Wand
Higher-order assembly language (HOAL) generalizes combinator-based target languages by allowing free variables in terms to play the role of registers, and the notion of a λ-representation is introduced, which is an abstract binding operation, and it is proved that the correctness of a compiler from a tiny language into HOAL is correct.
Type dispatch for named hierarchical types
44 Citations1999Neal Glew
A unifying mechanism, tagging, is described that abstracts the operation of class cast and class case constructs in object oriented languages, ML style exceptions, hierarchical extensible sums, and multimethods, and a small tagging language is formalised.
Partitioning dataflow analyses using types
40 Citations1997Erik Ruf
This work uses type information (either declared by the programmer, or computed via nonstandard type inference) to conservatively approximate analysis-time data dependences between program quantities, freeing us from the need to model all program quantities simultaneously in a single, monolithic analysis.
Semantics of memory management for polymorphic languages
38 Citations1999Greg Morrisett, Robert Harper
This work proves the soundness of the static semantics with respect to the dynamic semantics and shows how these same techniques may be used to establish thesoundness of various memory management strategies, including type-based, tag-free garbage collection; tailcall elimination; and environment strengthening.
Strongly Typed Flow-Directed Representation Transformations.
32 Citations1997Allyn Dimock, Robert Muller +2 more
Strongly typed flow-directed representation transformations (extended abstract)
28 Citations1997Allyn Dimock, Robert Muller +2 more
A new framework for transforming data representations in a strongly typed intermediate language that encompasses both closure conversion and inlining is presented and is adaptable to data other than functions.
Garbage collection for strongly-typed languages using run-time type reconstruction
26 Citations1994Shail Aditya, Christine H. Flood +1 more
This paper presents a new technique for live-object detection based on run-time type reconstruction for a strongly typed, polymorphic language and describes an implementation of the scheme for the Id parallel programming language compiled for the *T multiprocessor architecture.
Electronic Notes in Theoretical Computer ScienceTyped Closure Conversion for Recursively-Defined Functions
15 Citations1998Greg Morrisett, Robert Harper
Three main approaches are considered in the treatment of simply-typed closure conversion for compiler transformation to account for recursively-defined functions such as are found in ML, one based on a recursive code construct, oneBased on a self-referential data structure, and onebased on recursive types.
Foundations for the implementation of higher-order subtyping
13 Citations1997Karl Crary
It is shown how to implement a calculus with higher-order subtyping and subkinding by replacing uses of implicit subsumption with explicit coercions, and a polymorphic function is adjusted to take, as an additional argument, a proof that its type constructor argument has the desired kind.
From System F to Typed Assembly Language (Extended Version)
11 Citations1997Greg Morrisett, David Walker +2 more
ACM SIGPLAN Lisp PointersGarbage collection for strongly-typed languages using run-time type reconstruction
4 Citations1994Shail Aditya, Christine H. Flood +1 more