Precision in Practice: A Type-Preserving Java Compiler

Abstract

Popular mobile code architectures (Java and .NET) include verifiers to check for memory safety and other security properties. Since their formats are relatively high level, supporting a wide range of source language features is awkward. Further compilation and optimization, necessary for efficiency, must be trusted. We describe the design and implementation of a fully type-preserving compiler for Java and ML. Its strongly-typed intermediate language provides a low-level abstract machine model and a type system general enough to prove the safety of a variety of implementation techniques. We show that precise type preservation is within reach for real-world Java systems.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2005
Accession Number
ADA436468

Entities

People

  • Christopher League
  • Valery Trifonov
  • Zhong Shao

Organizations

  • Long Island University

Tags

Communities of Interest

  • Cyber

DTIC Thesaurus Topics

  • Abstracts
  • Assembly Languages
  • Coding
  • Compilers
  • Computer Program Documentation
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Instructions
  • Language
  • Machine Languages
  • New Jersey
  • Object Code
  • Optimization
  • Security
  • Standards

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Parallel and Distributed Computing.
  • Systems Analysis and Design