Type systems for useless-variable elimination

Adam Fischbach, John Hannan

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

We present a type-based specification for useless-variable elimination for a higher-order, call-by-value functional language. Utilizing a weak form of dependent types, we introduce a mechanism for eliminating at runtime useless code that is not detectable statically. We prove the specifications sound and safe with respect to an operational semantics, ensuring that eliminated expressions contributed no observable behavior to the original program. We define an algorithm that implements useless-variable elimination without dependent types, and we prove this algorithm correct with respect to the specification.

Original languageEnglish (US)
Pages (from-to)25-38
Number of pages14
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2053
DOIs
StatePublished - Jan 1 2001

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Type systems for useless-variable elimination'. Together they form a unique fingerprint.

Cite this