@article {19587,
	title = {From Principles to Practice with Class in the First Year},
	journal = {arXiv:1306.4713 [cs]},
	year = {2013},
	month = {2013/06/19/},
	abstract = {We propose a bridge between functional and object-oriented programming in the first-year curriculum. Traditionally, curricula that begin with functional programming transition to a professional, usually object-oriented, language in the second course. This transition poses obstacles for students, and often results in confusing the details of development environments, syntax, and libraries with the fundamentals of OO programming that the course should focus on. Instead, we propose to begin the second course with a sequence of custom teaching languages which minimize the transition from the first course, and allow students to focus on core ideas. After working through the sequence of pedagogical languages, we then transition to Java, at which point students have a strong command of the basic principles. We have 3 years of experience with this course, with notable success.},
	keywords = {Computer Science - Programming Languages},
	url = {http://arxiv.org/abs/1306.4713},
	author = {Tobin-Hochstadt, Sam and David Van Horn}
}
@article {19590,
	title = {Optimizing Abstract Abstract Machines},
	journal = {arXiv:1211.3722 [cs]},
	year = {2013},
	note = {Comment: Proceedings of the International Conference on Functional Programming 2013 (ICFP 2013). Boston, Massachusetts. September, 2013},
	month = {2013///},
	abstract = {The technique of abstracting abstract machines (AAM) provides a systematic approach for deriving computable approximations of evaluators that are easily proved sound. This article contributes a complementary step-by-step process for subsequently going from a naive analyzer derived under the AAM approach, to an efficient and correct implementation. The end result of the process is a two to three order-of-magnitude improvement over the systematically derived analyzer, making it competitive with hand-optimized implementations that compute fundamentally less precise results.},
	keywords = {Computer Science - Programming Languages, F.3.2},
	url = {http://arxiv.org/abs/1211.3722},
	author = {Johnson, J. Ian and Labich, Nicholas and Might, Matthew and David Van Horn}
}
@article {19589,
	title = {Introspective Pushdown Analysis of Higher-Order Programs},
	journal = {arXiv:1207.1813 [cs]},
	year = {2012},
	note = {Comment: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, 2012, ACM},
	month = {2012/07/07/},
	abstract = {In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. This work illuminates and conquers the theoretical challenges that stand in the way of combining the power of these techniques. The challenge in marrying these techniques is not subtle: computing the reachable control states of a pushdown system relies on limiting access during transition to the top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to compute a root set, just as concrete collection does. \emph{Introspective} pushdown systems resolve this conflict. Introspective pushdown systems provide enough access to the stack to allow abstract garbage collection, but they remain restricted enough to compute control-state reachability, thereby enabling the sound and precise product of pushdown analysis and abstract garbage collection. Experiments reveal synergistic interplay between the techniques, and the fusion demonstrates "better-than-both-worlds" precision.},
	keywords = {Computer Science - Programming Languages, D.3.4, F.3.2},
	url = {http://arxiv.org/abs/1207.1813},
	author = {Earl, Christopher and Sergey, Ilya and Might, Matthew and David Van Horn}
}
@article {19583,
	title = {Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis},
	journal = {arXiv:1105.1743 [cs]},
	year = {2011},
	note = {Comment: Communications of the ACM, Research Highlight},
	month = {2011/05/09/},
	abstract = {Predictive models are fundamental to engineering reliable software systems. However, designing conservative, computable approximations for the behavior of programs (static analyses) remains a difficult and error-prone process for modern high-level programming languages. What analysis designers need is a principled method for navigating the gap between semantics and analytic models: analysis designers need a method that tames the interaction of complex languages features such as higher-order functions, recursion, exceptions, continuations, objects and dynamic allocation. We contribute a systematic approach to program analysis that yields novel and transparently sound static analyses. Our approach relies on existing derivational techniques to transform high-level language semantics into low-level deterministic state-transition systems (with potentially infinite state spaces). We then perform a series of simple machine refactorings to obtain a sound, computable approximation, which takes the form of a non-deterministic state-transition systems with finite state spaces. The approach scales up uniformly to enable program analysis of realistic language features, including higher-order functions, tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.},
	keywords = {Computer Science - Programming Languages, F.3.2, F.4.1},
	url = {http://arxiv.org/abs/1105.1743},
	author = {David Van Horn and Might, Matthew}
}
@article {19580,
	title = {A family of abstract interpretations for static analysis of concurrent higher-order programs},
	journal = {arXiv:1103.5167 [cs]},
	year = {2011},
	note = {Comment: The 18th International Static Analysis Symposium (SAS 2011)},
	month = {2011/03/26/},
	abstract = {We develop a framework for computing two foundational analyses for concurrent higher-order programs: (control-)flow analysis (CFA) and may-happen-in-parallel analysis (MHP). We pay special attention to the unique challenges posed by the unrestricted mixture of first-class continuations and dynamically spawned threads. To set the stage, we formulate a concrete model of concurrent higher-order programs: the P(CEK*)S machine. We find that the systematic abstract interpretation of this machine is capable of computing both flow and MHP analyses. Yet, a closer examination finds that the precision for MHP is poor. As a remedy, we adapt a shape analytic technique-singleton abstraction-to dynamically spawned threads (as opposed to objects in the heap). We then show that if MHP analysis is not of interest, we can substantially accelerate the computation of flow analysis alone by collapsing thread interleavings with a second layer of abstraction.},
	keywords = {Computer Science - Programming Languages},
	url = {http://arxiv.org/abs/1103.5167},
	author = {Might, Matthew and David Van Horn}
}
@article {19588,
	title = {Higher-Order Symbolic Execution via Contracts},
	journal = {arXiv:1103.1362 [cs]},
	year = {2011},
	month = {2011/03/07/},
	abstract = {We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, enabling symbolic approximation of higher-order behavior. Our approach is based on the idea of an abstract reduction semantics that gives an operational semantics to programs with both concrete and symbolic components. Symbolic components are approximated by their contract and our semantics gives an operational interpretation of contracts-as-values. The result is a executable semantics that soundly predicts program behavior, including contract failures, for all possible instantiations of symbolic components. We show that our approach scales to an expressive language of contracts including arbitrary programs embedded as predicates, dependent function contracts, and recursive contracts. Supporting this feature-rich language of specifications leads to powerful symbolic reasoning using existing program assertions. We then apply our approach to produce a verifier for contract correctness of components, including a sound and computable approximation to our semantics that facilitates fully automated contract verification. Our implementation is capable of verifying contracts expressed in existing programs, and of justifying valuable contract-elimination optimizations.},
	keywords = {Computer Science - Programming Languages},
	url = {http://arxiv.org/abs/1103.1362},
	author = {Tobin-Hochstadt, Sam and David Van Horn}
}
@article {19594,
	title = {Semantic Solutions to Program Analysis Problems},
	journal = {arXiv:1105.0106 [cs]},
	year = {2011},
	month = {2011/04/30/},
	abstract = {Problems in program analysis can be solved by developing novel program semantics and deriving abstractions conventionally. For over thirty years, higher-order program analysis has been sold as a hard problem. Its solutions have required ingenuity and complex models of approximation. We claim that this difficulty is due to premature focus on abstraction and propose a new approach that emphasizes semantics. Its simplicity enables new analyses that are beyond the current state of the art.},
	keywords = {Computer Science - Programming Languages},
	url = {http://arxiv.org/abs/1105.0106},
	author = {Tobin-Hochstadt, Sam and David Van Horn}
}
@article {19595,
	title = {Systematic Abstraction of Abstract Machines},
	journal = {arXiv:1107.3539 [cs]},
	year = {2011},
	month = {2011/07/18/},
	abstract = {We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines for higher-order and imperative programming languages. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman, a lazy variant of Krivine{\textquoteright}s machine, and the stack-inspecting CM machine of Clements and Felleisen into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique of store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection. In order to close the gap between formalism and implementation, we provide translations of the mathematics as running Haskell code for the initial development of our method.},
	keywords = {Computer Science - Programming Languages},
	url = {http://arxiv.org/abs/1107.3539},
	author = {David Van Horn and Might, Matthew}
}
@article {19582,
	title = {Abstracting Abstract Machines},
	journal = {arXiv:1007.4446 [cs]},
	year = {2010},
	note = {Comment: The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP{\textquoteright}10), Baltimore, Maryland, September, 2010},
	month = {2010/07/26/},
	abstract = {We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman, a lazy variant of Krivine{\textquoteright}s machine, and the stack-inspecting CM machine of Clements and Felleisen into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique we call store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.},
	keywords = {Computer Science - Programming Languages, F.3.2, F.4.1},
	url = {http://arxiv.org/abs/1007.4446},
	author = {David Van Horn and Might, Matthew}
}
@article {19585,
	title = {Evaluating Call-By-Need on the Control Stack},
	journal = {arXiv:1009.3174 [cs]},
	year = {2010},
	note = {Comment: Symposium on Trends in Functional Programming (TFP 2010), Norman, Oklahoma, May 2010},
	month = {2010/09/16/},
	abstract = {Ariola and Felleisen{\textquoteright}s call-by-need {\lambda}-calculus replaces a variable occurrence with its value at the last possible moment. To support this gradual notion of substitution, function applications-once established-are never discharged. In this paper we show how to translate this notion of reduction into an abstract machine that resolves variable references via the control stack. In particular, the machine uses the static address of a variable occurrence to extract its current value from the dynamic control stack.},
	keywords = {Computer Science - Programming Languages, D.3.1},
	url = {http://arxiv.org/abs/1009.3174},
	author = {Chang, Stephen and David Van Horn and Felleisen, Matthias}
}
@article {19591,
	title = {Pushdown Control-Flow Analysis of Higher-Order Programs},
	journal = {arXiv:1007.4268 [cs]},
	year = {2010},
	note = {Comment: The 2010 Workshop on Scheme and Functional Programming},
	month = {2010/07/24/},
	abstract = {Context-free approaches to static analysis gain precision over classical approaches by perfectly matching returns to call sites---a property that eliminates spurious interprocedural paths. Vardoulakis and Shivers{\textquoteright}s recent formulation of CFA2 showed that it is possible (if expensive) to apply context-free methods to higher-order languages and gain the same boost in precision achieved over first-order programs. To this young body of work on context-free analysis of higher-order programs, we contribute a pushdown control-flow analysis framework, which we derive as an abstract interpretation of a CESK machine with an unbounded stack. One instantiation of this framework marks the first polyvariant pushdown analysis of higher-order programs; another marks the first polynomial-time analysis. In the end, we arrive at a framework for control-flow analysis that can efficiently compute pushdown generalizations of classical control-flow analyses.},
	keywords = {Computer Science - Programming Languages, F.3.2, F.4.1},
	url = {http://arxiv.org/abs/1007.4268},
	author = {Earl, Christopher and Might, Matthew and David Van Horn}
}
