From system F to typed assembly language
ACM Transactions on Programming Languages and SystemsPublished 1 May 1999Open access
Greg Morrisett, David Walker, Karl Crary, Neal Glew
Citations587
SJR quartileQ2
SJR score0.56
SNIP1.52
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 compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.
Abstract
We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. 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 lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.