Toward introducing binding-time analysis to MetaOCaml

3 years 11 days ago
Toward introducing binding-time analysis to MetaOCaml
This paper relates 2-level λ-calculus and staged λ-calculus (restricted to 2 stages) to obtain monovariant binding-time analysis for λ-calculus that produces the output in the form of staging annotations. The relationship between the two λ-calculi provides us with a precise and easy instruction on how to implement bindingtime analysis to be incorporated in the staged λ-calculus. It forms a basis for introducing binding-time analysis to full-fledged staged languages such as MetaOCaml. Categories and Subject Descriptors F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—Partial evaluation; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Lambda calculus and related systems General Terms Languages Keywords Partial evaluation, binding-time analysis, staging, 2level lambda-calculus, MetaOCaml
Kenichi Asai
Added 08 Apr 2016
Updated 08 Apr 2016
Type Journal
Year 2016
Where PEPM
Authors Kenichi Asai
Comments (0)