total 3936took 0.11s

Do Energy-oriented Changes Hinder Maintainability?Aug 22 2019Energy efficiency is a crucial quality requirement for mobile applications. However, improving energy efficiency is far from trivial as developers lack the knowledge and tools to aid in this activity. In this paper we study the impact of changes to improve ... More

Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational SemanticsAug 22 2019This volume contains the proceedings of EXPRESS/SOS 2019: the Combined 26th International Workshop on Expressiveness in Concurrency and the 16th Workshop on Structural Operational Semantics, which was held on August 26, 2019, in Amsterdam (The Netherlands), ... More

Scala Implicits are Everywhere: A large-scale study of the use of Implicits in the wildAug 21 2019Aug 22 2019The Scala programming language offers two distinctive language features implicit parameters and implicit conversions, often referred together as implicits. Announced without fanfare in 2004, implicits have quickly grown to become a widely and pervasively ... More

Scala Implicits are Everywhere: A large-scale study of the use of Implicits in the wildAug 21 2019The Scala programming language offers two distinctive language features implicit parameters and implicit conversions, often referred together as implicits. Announced without fanfare in 2004, implicits have quickly grown to become a widely and pervasively ... More

Free Theorems Simply, via DinaturalityAug 21 2019Free theorems are a popular tool in reasoning about parametrically polymorphic code. They are also of instructive use in teaching. Their derivation, though, can be tedious, as it involves unfolding a lot of definitions, then hoping to be able to simplify ... More

Reactive Probabilistic ProgrammingAug 20 2019Synchronous reactive languages were introduced for designing and implementing real-time control software. These domain-specific languages allow for writing a modular and mathematically precise specification of the system, enabling a user to simulate, ... More

Polyvariant Program Specialisation with Property-based AbstractionAug 20 2019In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation ... More

Lemma Generation for Horn Clause Satisfiability: A Preliminary StudyAug 20 2019It is known that the verification of imperative, functional, and logic programs can be reduced to the satisfiability of constrained Horn clauses (CHCs), and this satisfiability check can be performed by using CHC solvers, such as Eldarica and Z3. These ... More

Implicit Recursive Characteristics of STOPAug 19 2019The most important notations of Communicating Sequential Process(CSP) are the process and the prefix (event)$\rightarrow$(process) operator. While we can formally apply the $\rightarrow$ operator to define a live process's behavior, the STOP process, ... More

Implicit Recursive Characteristics of STOPAug 19 2019Aug 21 2019The most important notations of Communicating Sequential Process(CSP) are the process and the prefix (event)$\rightarrow$(process) operator. While we can formally apply the $\rightarrow$ operator to define a live process's behavior, the STOP process, ... More

A Symbolic Neural Network Representation and its Application to Understanding, Verifying, and Patching NetworkAug 17 2019Analysis and manipulation of trained neural networks is a challenging and important problem. We propose a symbolic representation for piecewise-linear neural networks and discuss its efficient computation. With this representation, one can translate the ... More

A Gentzen-style monadic translation of Gödel's System TAug 16 2019We present a monadic translation of G\"odel's System T in the spirit of Gentzen's negative translation, allowing us to reveal various structures of terms of System T.

Proceedings Seventh International Workshop on Verification and Program TransformationAug 16 2019This volume contains a final and revised selection of papers presented at the Seventh International Workshop on Verification and Program Transformation (VPT 2019), which took place in Genova, Italy, on April 2nd, 2019, affiliated with Programming 2019. ... More

Memory-Efficient Object-Oriented Programming on GPUsAug 16 2019Object-oriented programming is often regarded as too inefficient for high-performance computing (HPC), despite the fact that many important HPC problems have an inherent object structure. Our goal is to bring efficient, object-oriented programming to ... More

Bidirectional TypingAug 16 2019Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to break the decidability barrier ... More

Modular Verification of Heap Reachability Properties in Separation LogicAug 16 2019The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification ... More

CLOTHO: Directed Test Generation for Weakly Consistent Database SystemsAug 15 2019Relational database applications are notoriously difficult to test and debug. Concurrent execution of database transactions may violate complex structural invariants that constraint how changes to the contents of one (shared) table affect the contents ... More

Counting Immutable Beans: Reference Counting Optimized for Purely Functional ProgrammingAug 15 2019Most functional languages rely on some garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has less bookkeeping overhead at runtime. On the other hand, having an exact ... More

Toward Structured Proofs for Dynamic LogicsAug 15 2019We present Kaisar, a structured interactive proof language for differential dynamic logic (dL), for safety-critical cyber-physical systems (CPS). The defining feature of Kaisar is *nominal terms*, which simplify CPS proofs by making the frequently needed ... More

Undecidability of $D_{<:}$ and Its Decidable FragmentsAug 14 2019Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the calculus has been proven sound, it remains open whether type checking in DOT ... More

Type-two Iteration with Bounded Query RevisionAug 14 2019Motivated by recent results of Kapron and Steinberg (LICS 2018) we introduce new forms of iteration on length in the setting of applied lambda-calculi for higher-type poly-time computability. In particular, in a type-two setting, we consider functionals ... More

Type-Based Resource Analysis on HaskellAug 14 2019We propose an amortized analysis that approximates the resource usage of a Haskell expression. Using the plugin API of GHC, we convert the Haskell code into a simplified representation called GHC Core. We then apply a type-based system which derives linear ... More

Pointers in Recursion: Exploring the TropicsAug 14 2019We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are proven equivalent to the usual ... More

On the Elementary Affine Lambda-Calculus with and Without Fixed PointsAug 14 2019The elementary affine lambda-calculus was introduced as a polyvalent setting for implicit computational complexity, allowing for characterizations of polynomial time and hyperexponential time predicates. But these results rely on type fixpoints (a.k.a. ... More

Type-Directed Program Synthesis and Constraint Generation for Accelerator Library PortabilityAug 13 2019Fast numerical libraries have been a cornerstone of scientific computing for decades, but this comes at a price. Programs may be tied to vendor specific software ecosystems resulting in polluted, non-portable code. As we enter an era of heterogeneous ... More

Type-Directed Program Synthesis and Constraint Generation for Library PortabilityAug 13 2019Aug 14 2019Fast numerical libraries have been a cornerstone of scientific computing for decades, but this comes at a price. Programs may be tied to vendor specific software ecosystems resulting in polluted, non-portable code. As we enter an era of heterogeneous ... More

On the Complexity of Checking Transactional ConsistencyAug 13 2019Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and are resilient to failures. Modern databases provide different consistency models for transactions corresponding ... More

Introduction to the 35th International Conference on Logic Programming Special IssueAug 10 2019We are proud to introduce this special issue of Theory and Practice of Logic Programming (TPLP), dedicated to the regular papers accepted for the 35th International Conference on Logic Programming (ICLP). The ICLP meetings started in Marseille in 1982 ... More

The far side of the cubeAug 10 2019Game-semantic models usually start from the core model of the prototypical language PCF, which is characterised by a range of combinatorial constraints on the shape of plays. Relaxing each such constraint usually corresponds to the introduction of a new ... More

Functional programming with lambda-tree syntaxAug 09 2019We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders ... More

Multi-Modal Synthesis of Regular ExpressionsAug 09 2019Despite their usefulness across a wide range of application domains, regular expressions (or regexes for short) have a reputation for being difficult to master. In this paper, we propose a multi-modal synthesis technique for automatically synthesizing ... More

Multi-Modal Synthesis of Regular ExpressionsAug 09 2019Aug 12 2019Despite their usefulness across a wide range of application domains, regular expressions (or regexes for short) have a reputation for being difficult to master. In this paper, we propose a multi-modal synthesis technique for automatically synthesizing ... More

Manifest Contracts with Intersection TypesAug 08 2019We present a manifest contract system PCFv$\Delta$H with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a refinement type system and consistency of contracts is checked by ... More

Intrinsically-Typed Mechanized Semantics for Session TypesAug 08 2019Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages ... More

Sized Types for low-level Quantum MetaprogrammingAug 07 2019One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, ... More

Space-Efficient Gradual Typing in Coercion-Passing StyleAug 07 2019Herman et al. (2007, 2010) pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient ... More

A Transformational Approach to Resource Analysis with Typed-norms InferenceAug 06 2019In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that ... More

A Dependently Typed Multi-Stage CalculusAug 06 2019We study a dependently typed extension of a multi-stage programming language a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and eval for the execution of programs dynamically ... More

A minimal core calculus for Solidity contractsAug 06 2019The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles ... More

Circular Proofs as Session-Typed Processes: A Local Validity ConditionAug 06 2019Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between ... More

CREST: Hardware Formal Verification with ANSI-C Reference SpecificationsAug 04 2019This paper presents CREST, a prototype front-end tool intended as an add-on to commercial EDA formal verifcation environments. CREST is an adaptation of the CBMC bounded model checker for C, an academic tool widely used in industry for software analysis ... More

The meaning of a program change is a change to the program's meaningAug 02 2019Programming is the activity of modifying a program in order to bring about specific changes in its behaviour. Yet programming language theory almost exclusively focuses on the meaning of programs. We motivate a "change-oriented" viewpoint from which the ... More

Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)Aug 01 2019This work introduces the novel concept of kind refinement, which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles ... More

Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLPJul 31 2019CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming. In this adaptation, ... More

Aquarium Technical Report PreprintJul 31 2019In this technical report, we present the core calculi for two of the domain specific languages comprising the Aquarium kernel synthesis project. First, we present a machine modeling language named Cassiopea that is used to describe the semantics of individual ... More

VISCR: Intuitive & Conflict-free Automation for Securing the Dynamic Consumer IoT InfrastructuresJul 31 2019Consumer IoT is characterized by heterogeneous devices with diverse functionality and programming interfaces. This lack of homogeneity makes the integration and security management of IoT infrastructures a daunting task for users and administrators. In ... More

Towards a General Framework for Static Cost Analysis of Parallel Logic ProgramsJul 31 2019The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a wide variety of applications such as internet of things, cloud computing, ... More

Computing Abstract Distances in Logic ProgramsJul 30 2019Abstract interpretation is a well-established technique for performing static analyses of logic programs. However, choosing the abstract domain, widening, fixpoint, etc. that provides the best precision-cost trade-off remains an open problem. This is ... More

Compiling With Classical ConnectivesJul 30 2019The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice ... More

Proposition d'un modèle pour l'optimisation automatique de boucles dans le compilateur Tiramisu : cas d'optimisation de déroulageJul 29 2019Computer architectures become more and more complex. It requires more effort to develop techniques that improve the programs of performance and allow to exploit material resources efficiently. As a result, many transformations are applied on various levels ... More

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost AnalysisJul 29 2019Jul 31 2019Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, ... More

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost AnalysisJul 29 2019Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, ... More

Scalable Source Code Similarity Detection in Large Code RepositoriesJul 26 2019Source code similarity are increasingly used in application development to identify clones, isolate bugs, and find copy-rights violations. Similar code fragments can be very problematic due to the fact that errors in the original code must be fixed in ... More

Lazy Stream Programming in PrologJul 26 2019In recent years, stream processing has become a prominent approach for incrementally handling large amounts of data, with special support and libraries in many programming languages. Unfortunately, support in Prolog has so far been lacking and most existing ... More

An Introduction to Logical RelationsJul 25 2019Logical relations (LR) have been around for many years, and today they are used in many formal results. However, it can be difficult to LR beginners to find a good place to start to learn. Papers often use highly specialized LRs that use the latest advances ... More

Spacetime Programming: A Synchronous Language for Composable Search StrategiesJul 25 2019Search strategies are crucial to efficiently solve constraint satisfaction problems. However, programming search strategies in the existing constraint solvers is a daunting task and constraint-based languages usually have compositionality issues. We propose ... More

Symbolic Analysis of Maude Theories with NarvalJul 25 2019Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude's symbolic capabilities ... More

Applying Constraint Logic Programming to SQL Semantic AnalysisJul 25 2019This paper proposes the use of Constraint Logic Programming (CLP) to model SQL queries in a data-independent abstract layer by focusing on some semantic properties for signalling possible errors in such queries. First, we define a translation from SQL ... More

A Probabilistic Separation LogicJul 24 2019Probabilistic independence is a fundamental tool for reasoning about randomized programs. Independence describes the result of drawing a fresh random sample---a basic operation in all probabilistic languages---and greatly simplifies formal reasoning about ... More

Sketch-n-Sketch: Output-Directed Programming for SVGJul 24 2019For creative tasks, programmers face a choice: Use a GUI and sacrifice flexibility, or write code and sacrifice ergonomics? To obtain both flexibility and ease of use, a number of systems have explored a workflow that we call output-directed programming. ... More

Sketch-n-Sketch: Output-Directed Programming for SVGJul 24 2019Aug 10 2019For creative tasks, programmers face a choice: Use a GUI and sacrifice flexibility, or write code and sacrifice ergonomics? To obtain both flexibility and ease of use, a number of systems have explored a workflow that we call output-directed programming. ... More

Sketch-n-Sketch: Output-Directed Programming for SVGJul 24 2019Jul 30 2019For creative tasks, programmers face a choice: Use a GUI and sacrifice flexibility, or write code and sacrifice ergonomics? To obtain both flexibility and ease of use, a number of systems have explored a workflow that we call output-directed programming. ... More

Towards a Smart Contract Verification Framework in CoqJul 24 2019We propose a novel way of embedding functional smart contract languages into the Coq proof assistant using meta-programming techniques. Our framework allows for developing the meta-theory of smart contract languages using the deep embedding and provides ... More

A Case for Stale Synchronous Distributed Model for Declarative Recursive ComputationJul 24 2019A large class of traditional graph and data mining algorithms can be concisely expressed in Datalog, and other Logic-based languages, once aggregates are allowed in recursion. In fact, for most BigData algorithms, the difficult semantic issues raised ... More

Resource Analysis driven by (Conditional) Termination ProofsJul 23 2019When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. ... More

The Expressive Power of Higher-Order DatalogJul 23 2019Jul 24 2019A classical result in descriptive complexity theory states that Datalog expresses exactly the class of polynomially computable queries on ordered databases. In this paper we extend this result to the case of higher-order Datalog. In particular, we demonstrate ... More

Learning the Relation between Code Features and Code Transforms with Structured PredictionJul 22 2019We present in this paper the first approach for structurally predicting code transforms at the level of AST nodes using conditional random fields. Our approach first learns offline a probabilistic model that captures how certain code transforms are applied ... More

Towards meta-interpretive learning of programming language semanticsJul 20 2019We introduce a new application for inductive logic programming: learning the semantics of programming languages from example evaluations. In this short paper, we explored a simplified task in this domain using the Metagol meta-interpretive learning system. ... More

Towards Verified Stochastic Variational Inference for Probabilistic ProgramsJul 20 2019Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, ... More

Towards Verified Stochastic Variational Inference for Probabilistic ProgramsJul 20 2019Jul 25 2019Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, ... More

Online Set-Based Dynamic Analysis for Sound Predictive Race DetectionJul 19 2019Predictive data race detectors find data races that exist in executions other than the observed execution. Smaragdakis et al. introduced the causally-precedes (CP) relation and a polynomial-time analysis for sound (no false races) predictive data race ... More

Responsibility Analysis by Abstract InterpretationJul 18 2019Given a behavior of interest in the program, statically determining the corresponding responsible entity is a task of critical importance, especially in program security. Classical static analysis techniques (e.g. dependency analysis, taint analysis, ... More

Asynchronous Snapshots of Actor Systems for Latency-Sensitive ApplicationsJul 18 2019The actor model is popular for many types of server applications. Efficient snapshotting of applications is crucial in the deployment of pre-initialized applications or moving running applications to different machines, e.g for debugging purposes. A key ... More

Generating Correctness Proofs with Neural NetworksJul 17 2019Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cost of producing foundationally verified software remains prohibitively high ... More

Generating Correctness Proofs with Neural NetworksJul 17 2019Aug 06 2019Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cost of producing foundationally verified software remains prohibitively high ... More

ART: Abstraction Refinement-Guided Training for Provably Correct Neural NetworksJul 17 2019Jul 26 2019Artificial neural networks (ANNs) have demonstrated remarkable utility in a variety of challenging machine learning applications. However, their complex architecture makes asserting any formal guarantees about their behavior difficult. Existing approaches ... More

A Differentiable Programming System to Bridge Machine Learning and Scientific ComputingJul 17 2019Jul 18 2019Scientific computing is increasingly incorporating the advancements in machine learning and the ability to work with large amounts of data. At the same time, machine learning models are becoming increasingly sophisticated and exhibit many features often ... More

Zygote: A Differentiable Programming System to Bridge Machine Learning and Scientific ComputingJul 17 2019Scientific computing is increasingly incorporating the advancements in machine learning and the ability to work with large amounts of data. At the same time, machine learning models are becoming increasingly sophisticated and exhibit many features often ... More

Recovering Purity with Comonads and CapabilitiesJul 16 2019In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended ... More

Object-Capability as a Means of Permission and Authority in Software SystemsJul 16 2019The object-capability model is a security measure that consists in encoding access rights in individual objects to restrict its interactions with other objects. Since its introduction in 2013, different approaches to object-capability have been formalized ... More

A Relational Static Semantics for Call Graph ConstructionJul 15 2019The problem of resolving virtual method and interface calls in object-oriented languages has been a long standing challenge to the program analysis community. The complexities are due to various reasons, such as increased levels of class inheritance and ... More

Bayesian Synthesis of Probabilistic Programs for Automatic Data ModelingJul 14 2019We present new techniques for automatically constructing probabilistic programs for data analysis, interpretation, and prediction. These techniques work with probabilistic domain-specific data modeling languages that capture key properties of a broad ... More

Automatic Repair and Type Binding of Undeclared Variables using Neural NetworksJul 14 2019Deep learning had been used in program analysis for the prediction of hidden software defects using software defect datasets, security vulnerabilities using generative adversarial networks as well as identifying syntax errors by learning a trained neural ... More

Crumbling Abstract MachinesJul 13 2019Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications ... More

Language Support for Adaptation: Intent-Driven Programming in FASTJul 12 2019Historically, programming language semantics has focused on assigning a precise mathematical meaning to programs. That meaning is a function from the program's input domain to its output domain determined solely by its syntactic structure. Such a semantics, ... More

Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear TimeJul 12 2019Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and ... More

Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear TimeJul 12 2019Jul 16 2019Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and ... More

Verified Self-Explaining ComputationJul 12 2019Common programming tools, like compilers, debuggers, and IDEs, crucially rely on the ability to analyse program code to reason about its behaviour and properties. There has been a great deal of work on verifying compilers and static analyses, but far ... More

Mercem: Method Name Recommendation Based on Call Graph EmbeddingJul 12 2019Comprehensibility of source code is strongly affected by identifier names, therefore software developers need to give good (e.g. meaningful but short) names to identifiers. On the other hand, giving a good name is sometimes a difficult and time-consuming ... More

Augmenting Type Signatures for Program SynthesisJul 12 2019Effective program synthesis requires a way to minimise the number of candidate programs being searched. A type signature, for example, places some small restrictions on the structure of potential candidates. We introduce and motivate a distilled program ... More

Concolic Testing Heap-Manipulating ProgramsJul 12 2019Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on numeric programs. Heap-manipulating programs make extensive use of complex ... More

Revisiting Occurrence TypingJul 12 2019We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages. Although occurrence typing was tied from its inception to set-theoretic types-union ... More

Revisiting Occurrence TypingJul 12 2019Jul 15 2019We revisit occurrence typing, a technique to re ne the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages. Although occurrence typing was tied from its inception to set-theoretic types-union ... More

Revisiting Occurrence TypingJul 12 2019Jul 17 2019We revisit occurrence typing, a technique to re ne the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages. Although occurrence typing was tied from its inception to set-theoretic types-union ... More

Compositional Inference Metaprogramming with Convergence GuaranteesJul 11 2019Inference metaprogramming enables effective probabilistic programming by supporting the decomposition of executions of probabilistic programs into subproblems and the deployment of hybrid probabilistic inference algorithms that apply different probabilistic ... More

Compositional Inference Metaprogramming with Convergence GuaranteesJul 11 2019Jul 15 2019Inference metaprogramming enables effective probabilistic programming by supporting the decomposition of executions of probabilistic programs into subproblems and the deployment of hybrid probabilistic inference algorithms that apply different probabilistic ... More

Imitation-Projected Policy Gradient for Programmatic Reinforcement LearningJul 11 2019We present Imitation-Projected Policy Gradient (IPPG), an algorithmic framework for learning policies that are parsimoniously represented in a structured programming language. Such programmatic policies can be more interpretable, generalizable, and amenable ... More

Trace-Relating Compiler Correctness and Secure CompilationJul 11 2019Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, ... More

Trace-Relating Compiler Correctness and Secure CompilationJul 11 2019Jul 17 2019Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, ... More

Executable formal semantics for the POSIX shellJul 11 2019The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert's control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical ... More