Type systems for useless-variable elimination

Adam Fischbach; John Hannan

doi:10.1007/3-540-44978-7_3

Type systems for useless-variable elimination

Adam Fischbach, John Hannan

Computer Science and Engineering

Research output: Contribution to journal › Article › peer-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 language	English (US)
Pages (from-to)	25-38
Number of pages	14
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2053
DOIs	https://doi.org/10.1007/3-540-44978-7_3
State	Published - 2001

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-44978-7_3

Cite this

@article{3391f3ecf6d74a47b951f9c7851a0b6c,

title = "Type systems for useless-variable elimination",

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.",

author = "Adam Fischbach and John Hannan",

year = "2001",

doi = "10.1007/3-540-44978-7_3",

language = "English (US)",

volume = "2053",

pages = "25--38",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

}

TY - JOUR

T1 - Type systems for useless-variable elimination

AU - Fischbach, Adam

AU - Hannan, John

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84876636963&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84876636963&partnerID=8YFLogxK

U2 - 10.1007/3-540-44978-7_3

DO - 10.1007/3-540-44978-7_3

M3 - Article

AN - SCOPUS:84876636963

SN - 0302-9743

VL - 2053

SP - 25

EP - 38

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -

Type systems for useless-variable elimination

Abstract

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this