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

• Type: Journal
• Year: 2016
• Where: PEPM
• Authors: Kenichi Asai
• Keywords: PEPM 2016, Software Engineering