A Modal Analysis of Staged Computation,

Abstract

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main technical result is a conservative embedding of Nielson & Nielson's two-level functional language in our language Mini-ML, which in addition to partial evaluation also supports multiple computation stages, sharing of code across multiple stages, and run-time code generation. (AN)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1995
Accession Number
ADA296537

Entities

People

  • Frank Pfenning
  • Rowan Davies

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Calculus
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Demographic Cohorts
  • Inversion
  • Judgment
  • Language
  • Machine Languages
  • Modal Analysis
  • Programming Languages
  • Semantics
  • Specialization
  • Theoretical Computer Science
  • Translations

Fields of Study

  • Computer science

Readers

  • Computer Engineering
  • Distributed Systems and Data Platform Development
  • Operations Research