We present λ CIL , a typed λ-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of λ CIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since λ CIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.

The CIL compiler for core Standard ML compiles whole ML programs using a novel typed intermediate language that supports the generation of type-safe customized data representations. In this paper, we present empirical data comparing the relative efficacy of several different flow-based customization strategies for function representations. We develop a cost model to interpret dynamic counts of operations required for each strategy. In this cost model, customizing the representation of closed functions gives a 12-17% improvement on average over uniform closure representations, depending on the layout of the closure. We also present data on the relative effectiveness of various strategies for reducing representation pollution, i.e., situations where flow constraints require the representation of a value to be less efficient than it would be in ideal circumstances. For the benchmarks tested and the types of representation pollution detected by our compiler, the pollution removal strategies we consider often cost more in overhead than they gain via enabled customizations. Notable exceptions are selective defunctionalization, a function representation strategy that often achieves significant customization benefits via aggressive pollution removal, and a simple form of flow-directed inlining, in which pollution removal allows multiple functions to be inlined at the same call site.

We present a new framework for transforming data representations in a strongly typed intermediate language. Our method allows both value producers (sources) and value consumers (sinks) to support multiple representations, automatically inserting any required code. Specialized representations can be easily chosen for particular source/sink pairs.The framework is based on these techniques:1. Flow annotated types encode the "flows-from" (source) and "flows-to" (sink) information of a flow graph.2. Intersection and union types support (a) encoding precise flow information, (b) separating flow information so that transformations can be well typed, (c) automatically reorganizing flow paths to enable multiple representations.As an instance of our framework, we provide a function representation transformation that encompasses both closure conversion and inlining. Our framework is adaptable to data other than functions.

We develop a calculus in which the computation steps required to execute a computer program can be separated into discrete stages. The calculus, denoted λ2, is embedded within the pure untyped λ-calculus. The main result of the paper is a characterization of sufficient conditions for confluence for terms in the calculus. The condition can be taken as a correctness criterion for translators that perform reductions in one stage leaving residual redexes over for subsequent computation stages. As an application of the theory, we verify the correctness of a macro expansion algorithm. The expansion algorithm is of some interest in its own right since it solves the problem of desired variable capture using only the familiar capture avoiding substitutions.

Over the last several years, much interesting work has been done in modelling object-oriented programming languages in terms of extensions of the bounded second-order lambda calculus, F . Unfortunately, it has recently been shown by Pierce ([Pie92]) that type checking F is undecidable. Moreover, he showed that the undecidability arises in the seemingly simpler problem of determining whether one type is a subtype of another. In [Bru93a, Bru93b], the first author introduced a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variables, subtypes, and inheritance. The semantics of TOOPL is based on F , so the question arises whether type checking in this language is decidable. In this paper we show that type checking for TOOPLE, a minor variant of TOOPL (Typed Object-Oriented Programming Language), is decidable. The proof proceeds by showing that subtyping is decidable, that all terms of TOOPLE have minimum types...

In this paper we introduce M-LISP, a dialect of LISP designed with an eye toward reconciling LISP's metalinguistic power with the structural style of operational semantics advocated by Plotkin [28]. We begin by reviewing the original definition of LISP [20] in an attempt to clarify the source of its metalinguistic power. We find that it arises from a problematic clause in this definition. We then define the abstract syntax and operational semantics of M-LISP, essentially a hybrid of M-expression LISP and Scheme. Next, we tie the operational semantics to the corresponding equational logic. As usual, provable equality in the logic implies operational equality. Having established this framework we then extend M-LISP with the metalinguistic eval and reify operators (the latter is a nonstrict operator that converts its argument to its metalanguage representation). These operators encapsulate the matalinguistic representation conversions that occur globally in S-expression LISP. We show that the naive versions of these operators render LISP's equational logic inconsistent. On the positive side, we show that a naturally restricted form of the eval operator is confluent and therefore a conservative extension of M-LISP. Unfortunately, we must weaken the logic considerably to obtain a consistent theory of reification.

article Free Access Share on M-LISP: its natural semantics and equational logic Author: Robert Muller Aiken Computation Laboratory, Harvard University, Cambridge, MA Aiken Computation Laboratory, Harvard University, Cambridge, MAView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 9Sept. 1991 pp 234–242https://doi.org/10.1145/115866.115891Published:01 May 1991Publication History 0citation317DownloadsMetricsTotal Citations0Total Downloads317Last 12 Months26Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF