We bridge the gap between functional evaluators and abstract machines for lambda-calculus, using closure conversion, transformation into continuation-passing style, defunctionalization of continuations.<br /> <br />We illustrate this by deriving Krivine's machine from an ordinary call-by-name evaluator call-by-value Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in literature. second one new. Together, they show that correspond...

We bridge the gap between functional evaluators and abstract machines for λ-calculus, using closure conversion, transformation into continuation-passing style, defunctionalization.We illustrate this approach by deriving Krivine's machine from an ordinary call-by-name evaluator call-by-value Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in literature. second one new. Together, they show that correspond to facets of λ-calculus.We then reveal...

We show how to derive a compiler and virtual machine from compositional interpreter. first illustrate the derivation with two evaluation functions normalization functions. obtain Krivine's machine, Felleisen et al.'s CEK generalization of these machines performing strong normalization, which is new. observe that several existing compilers machines--e.g., Categorical Abstract Machine (CAM), Schmidt's VEC Leroy's Zinc abstract machine--are already in derived form we present corresponding...

We derive a control-flow analysis that approximates the interprocedural of both function calls and returns in presence first-class functions tail-call optimization. In addition to an abstract environment, our computes for each expression control stack, effectively approximating where return across optimized tail calls. The is systematically calculated by interpretation stack-based CaEK machine Flanagan et al. using series Galois connections. Abstract provides unifying setting which we 1)...

Recent developments in the systematic construction of abstract interpreters hinted at possibility a broad unification concepts static analysis. We deliver that by showing context-sensitivity, polyvariance, flow-sensitivity, reachability-pruning, heap-cloning and cardinality-bounding to be independent any particular semantics. Monads become unifying agent between these For instance, plugging same "context-insensitivity monad" into monadically-parameterized semantics for Java or lambda...

How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of language. But in statically-typed such as OCaml too many these candidate will be rejected ill-typed by type checker. As refinement Pałka et al. propose goal-directed, bottom-up reading up typing relation. We have written generator. However generated has output that depend on evaluation order, which commonly under-specified languages OCaml,...

Summary A static analysis can check programs for potential errors. natural question that arises is therefore: who checks the checker? Researchers have given this varying attention, ranging from basic testing techniques, informal monotonicity arguments, thorough pen‐and‐paper soundness proofs, to verified fixed point checking. In paper, we demonstrate how quickchecking be useful test a range of properties with limited effort. We show algebraic lattice properties, help ensure an implementation...

A recent line of work lifts particular verification and analysis methods to Software Product Lines (SPL). In an effort generalize such case-by-case approaches, we develop a systematic methodology for lifting program analyses SPLs using abstract interpretation. Abstract interpretation is classical framework deriving static in compositional, step-by-step manner. We show how take expressed as lift each the steps family programs. This includes schemes domain types, combinators Galois...

We extend our correspondence between evaluators and abstract machines from the pure setting of lambda-calculus to impure computational lambda-calculus. show how derive new monadic for Starting (1) a generic evaluator parameterized by monad (2) specifying effect, we inline components in obtain an written style that is specific this effect. then corresponding machine closure-converting, CPS-transforming, defunctionalizing evaluator. illustrate construction first with identity monad, obtaining...

A static analysis can check programs for potential errors. natural question that arises is therefore: who checks the checker? Researchers have given this varying attention, ranging from basic testing techniques, informal monotonicity arguments, thorough pen-and-paper soundness proofs, to verified fixed point checking. In paper we demonstrate how quickchecking be useful a range of properties with limited effort. We show algebraic lattice properties, help ensure an implementation follows...

We present a survey of control-flow analysis functional programs, which has been the subject extensive investigation throughout past 25 years. Analyses control flow programs have formulated in multiple settings and led to many different approximations, starting with seminal works Jones, Shivers, Sestoft. In this paper we by structuring multitude formulations approximations comparing them.

The flexibility of dynamically typed languages such as JavaScript, Python, Ruby, and Scheme comes at the cost run-time type checks. Some these checks can be eliminated via control-flow analysis. However, traditional analysis (CFA) is not ideal for this task it ignores flow-sensitive information that gained from dynamic predicates, JavaScript's 'instanceof' Scheme's 'pair?', type-restricted operators, 'car'. Yet, adding flow-sensitivity to a CFA worsens already significant compile-time CFA....

We extend our correspondence between evaluators and abstract machines from the pure setting of lambda-calculus to impure computational lambda-calculus. Specifically, we show how derive new monadic for Starting a evaluator given monad, inline components monad in corresponding machine by closure-converting, CPS-transforming, defunctionalizing this inlined interpreter. illustrate construction first with identity obtaining yet again CEK machine, then state an exception combination both.<br...

No abstract available.