the proceedings contain 26 papers. the special focus in this conference is on Compilers and Separation Logic. the topics include: Memory-efficient tail calls in the JVM with imperative functional objects;a secure comp...
ISBN:
(纸本)9783319265285
the proceedings contain 26 papers. the special focus in this conference is on Compilers and Separation Logic. the topics include: Memory-efficient tail calls in the JVM with imperative functional objects;a secure compiler for ML modules;a complete and polynomial-time algorithm in SSA;separation logic with monadic inductive definitions and implicit existentials;tree-like grammars and separation logic;randomized resource-aware path-sensitive static analysis;an extension of zonotopes to quadratic arithmetics;abstraction of optional numerical values;fault-tolerant resource reasoning;a blame calculus with delimited control;aliasing control in an imperative pure calculus;a strong distillery;from call-by-value to interaction by typed closure conversion;a marriage of game semantics and operational techniques;automata-based abstraction for automated verification of higher-order tree-processing programs;decision algorithms for checking definability of order-2 finitary PCF;uncovering javascript performance code smells relevant to type mutations;analyzing distributed multi-platform java and android applications with shadowVM;quasi-linearizability is undecidable;objects in polynomial time;programming techniques for reversible comparison sorts;transactions on mergeable objects;a sound type system for layer subtyping and dynamically activated first-class layers;bottom-up context-sensitive pointer analysis for java and more sound static handling of java reflection.
We study the efficient implementation of call-by-value using the structure of interactive computation models. this structure has been useful in applications to resource-bounded compilation, but much of the existing wo...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
We study the efficient implementation of call-by-value using the structure of interactive computation models. this structure has been useful in applications to resource-bounded compilation, but much of the existing work in this area has focused on call-by-name programminglanguages. this paper works towards the goal of a simple, efficient treatment of call-by-value languages. In previous work we have studied cps-translation as an approach to implementing call-by-value and have observed that it needs to be refined in order to achieve efficient space usage. In this paper we give an alternative presentation of the refined translation, which is close to existing methods of typed closure conversion. We show that a simple correctness proof following Benton and Hur is possible for this formulation. Moreover, we extend previous work to cover full recursion in the source language.
Separation Logic with inductive predicate definitions (SL) and hyperedge replacement grammars (HRG) are established formalisms to describe the abstract shape of data structures maintained by heap-manipulating programs...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
Separation Logic with inductive predicate definitions (SL) and hyperedge replacement grammars (HRG) are established formalisms to describe the abstract shape of data structures maintained by heap-manipulating programs. Fragments of both formalisms are known to coincide, and neither the entailment problem for SL nor its counterpart for HRGs, the inclusion problem, are decidable in general. We introduce tree-like grammars (TLG), a fragment of HRGs with a decidable inclusion problem. By the correspondence between HRGs and SL, we simultaneously obtain an equivalent SL fragment (SLtl) featuring some remarkable properties including a decidable entailment problem.
A common approach to reversible programming is to reversibly simulate an irreversible program withthe desired functionality, which in general puts additional pressure on the computational resources (time, space.) If ...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
A common approach to reversible programming is to reversibly simulate an irreversible program withthe desired functionality, which in general puts additional pressure on the computational resources (time, space.) If the same running time is required, ensuring a minimal space overhead is a significant programming challenge. We introduce criteria for the optimality of reversible simulation: A reversible simulation is faithful if it incurs no asymptotic time overhead and bounds the space overhead (the garbage) by some function g(n), and hygienic if g is (asymptotically) optimal for faithful simulation. We demonstrate the programming techniques used to develop faithful and hygienic reversible simulations of several well-known comparison sorts, e.g. insertion sort and quicksort, using representations of permutations in boththe output and intermediate additional space required.
Destructible updates on shared objects require careful handling of concurrent accesses in multi-threaded programs. Paradigms such as Transactional Memory support the programmer in correctly synchronizing access to mut...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
Destructible updates on shared objects require careful handling of concurrent accesses in multi-threaded programs. Paradigms such as Transactional Memory support the programmer in correctly synchronizing access to mutable shared data by serializing the transactional reads and writes. But under high contention, serializable transactions incur frequent aborts and limit parallelism. this can lead to a severe performance degradation. In this paper, we propose mergeable transactions which provide a consistency semantics that allows for more scalability even under contention. Instead of aborting and re-executing, object versions from conflicting updates on shared objects are merged using data-type specific semantics. the evaluation of our prototype implementation in Haskell shows that mergeable transactions outperform serializable transactions even under low contention while providing a structured and type-safe interface.
this paper presents FCore: a JVM implementation of System F with support for full tail-call elimination (TCE). Our compilation technique for FCore is innovative in two respects: it uses a new representation for first-...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
this paper presents FCore: a JVM implementation of System F with support for full tail-call elimination (TCE). Our compilation technique for FCore is innovative in two respects: it uses a new representation for first-class functions called imperative functional objects;and it provides a way to do TCE on the JVM using constant space. Unlike conventional TCE techniques on the JVM, allocated function objects are reused in chains of tail calls. thus, programs written in FCore can use idiomatic functional programming styles, relying on TCE, and perform well without worrying about the JVM limitations. Our empirical results show that programs which use tail calls can run in constant space and with low execution time overhead when compiled with FCore.
the machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languag...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
the machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programminglanguages. this paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. the study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.
the vast amount of code available on the web is increasing on a daily basis. Open-source hosting sites such as Github contain billions of lines of code. Community question-answering sites provide millions of code snip...
详细信息
ISBN:
(纸本)9783319265292;9783319265285
the vast amount of code available on the web is increasing on a daily basis. Open-source hosting sites such as Github contain billions of lines of code. Community question-answering sites provide millions of code snippets with corresponding text and metadata. the amount of code available in executable binaries is even greater. In this talk, I will cover recent research trends on leveraging such "big code" for program analysis, program synthesis and reverse engineering. We will consider a range of semantic representations based on symbolic automata [11,15], tracelets [3], numerical abstractions [13,14], and textual descriptions [1,22], as well as different notions of code similarity based on these representations. To leverage these semantic representations, we will consider a number of prediction techniques, including statistical language models [19,20], variable order Markov models [2], and other distance-based and model-based sequence classification techniques. Finally, I will show applications of these techniques including semantic code search in both source code and stripped binaries, code completion and reverse engineering.
暂无评论