Latest in cs.pl
total 3336took 0.17s
Compiling for Encrypted Computing: Obfuscation but Not in NameApr 20 2019Encrypted computing is the emerging science and technology of processors that take encrypted inputs to encrypted outputs via encrypted intermediates (at nearly conventional speeds). The aim is to make user data in general-purpose computing secure against ... More ClangJIT: Enhancing C++ with Just-in-Time CompilationApr 18 2019The C++ programming language is not only a keystone of the high-performance-computing ecosystem but has proven to be a successful base for portable parallel-programming frameworks. As is well known, C++ programmers use templates to specialize algorithms, ... More Relay: A High-Level IR for Deep LearningApr 17 2019Frameworks for writing, compiling, and optimizing deep learning (DL) models have recently enabled progress in areas like computer vision and natural language processing. Extending these frameworks to accommodate the rapidly diversifying landscape of DL ... More On Resolving Non-determinism in ChoreographiesApr 17 2019Choreographies specify multiparty interactions via message passing. A \emph{realization} of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies ... More Scalable Verification of Probabilistic NetworksApr 17 2019This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This ... More A 2-Categorical Study of Graded and Indexed MonadsApr 17 2019In the study of computational effects, it is important to consider the notion of computational effects with parameters. The need of such a notion arises when, for example, statically estimating the range of effects caused by a program, or studying the ... More Using Dynamic Analysis to Generate Disjunctive InvariantsApr 16 2019Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. ... More The Geometry of Bayesian ProgrammingApr 16 2019We give a geometry of interaction model for a typed lambda-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based ... More Resource-Guided Program SynthesisApr 16 2019Apr 18 2019This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines ... More Resource-Guided Program SynthesisApr 16 2019This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines ... More A Path To DOT: Formalizing Fully-Path-Dependent TypesApr 15 2019The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types $-$ types such as $x.a_1\dots a_n.T$ that depend on the runtime value of a path $x.a_1\dots a_n$ to an object. Unfortunately, ... More Taking Linear Logic ApartApr 15 2019Process calculi based on logic, such as $\pi$DILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the $\pi$-calculus: ... More On the Lambek Calculus with an Exchange ModalityApr 15 2019In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic ... More From Linear Logic to Cyclic SharingApr 15 2019We present a translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing. This translation is derived from a simple observation on the Int-construction on traced monoidal categories. It turns out that ... More The Bang Calculus and the Two Girard's TranslationsApr 15 2019We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both call-by-name and call-by-value lambda-calculi to ... More Got: Git, but for ObjectsApr 13 2019We look at one important category of distributed applications characterized by the existence of multiple collaborating, and competing, components sharing mutable, long-lived, replicated objects. The problem addressed by our work is that of object state ... More Flint for Safer Smart ContractsApr 13 2019The Ethereum blockchain platform supports the execution of decentralised applications or smart contracts. These typically hold and transfer digital currency to other parties on the platform; however, they have been subject to numerous attacks due to the ... More SyGuS-Comp 2018: Results and AnalysisApr 12 2019Syntax-guided synthesis (SyGuS) is the computational problem of finding an implementation $f$ that meets both a semantic constraint given by a logical formula $\phi$ in a background theory $\mathbb{T}$, and a syntactic constraint given by a grammar $G$, ... More Verified Optimization in a Quantum Intermediate RepresentationApr 12 2019We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate ... More Synthesizing Database Programs for Schema RefactoringApr 11 2019Many programs that interact with a database need to undergo schema refactoring several times during their life cycle. Since this process typically requires making significant changes to the program's implementation, schema refactoring is often non-trivial ... More A HoTT Quantum Equational Theory (Extended Version)Apr 08 2019This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approach is highly expressive, and reflects the style of state-of-the art quantum ... More Verification Logics for Quantum ProgramsApr 08 2019We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare ... More Type-Level Computations for Ruby LibrariesApr 06 2019Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often arises when using certain Ruby libraries. For example, the type safety of a ... More A Literature Study of Embeddings on Source CodeApr 05 2019Natural language processing has improved tremendously after the success of word embedding techniques such as word2vec. Recently, the same idea has been applied on source code with encouraging results. In this survey, we aim to collect and discuss the ... More Proving tree algorithms for succinct data structuresApr 04 2019Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different ... More Symbolic Exact Inference for Discrete Probabilistic ProgramsApr 03 2019The computational burden of probabilistic inference remains a hurdle for applying probabilistic programming languages to practical problems of interest. In this work, we provide a semantic and algorithmic foundation for efficient exact inference on discrete-valued ... More Symbolic Exact Inference for Discrete Probabilistic ProgramsApr 03 2019Apr 11 2019The computational burden of probabilistic inference remains a hurdle for applying probabilistic programming languages to practical problems of interest. In this work, we provide a semantic and algorithmic foundation for efficient exact inference on discrete-valued ... More A Message-Passing Interpretation of Adjoint LogicApr 02 2019We present a system of session types based on adjoint logic which generalize standard binary session types. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, ... More Value-Dependent Session Design in a Dependently Typed LanguageApr 02 2019Session Types offer a typing discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care ... More Concurrent Typestate-Oriented Programming in JavaApr 02 2019We describe a generative approach that enables concurrent typestate-oriented programming in Java and other mainstream languages. The approach allows programmers to implement objects exposing a state-sensitive interface using a high-level synchronization ... More FreeST: Context-free Session Types in a Functional LanguageApr 02 2019FreeST is an experimental concurrent programming language. Based on a core linear functional programming language, it features primitives to fork new threads, and for channel creation and communication. A powerful type system of context-free session types ... More Service Equivalence via Multiparty Session Type IsomorphismsApr 02 2019This paper addresses a problem found within the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We utilise the theory of Multiparty ... More A benchmark for C program verificationApr 01 2019We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last ... More A Provable Defense for Deep Residual NetworksMar 29 2019We present a training system, which can provably defend significantly larger neural networks than previously possible, including ResNet-34 and DenseNet-100. Our approach is based on differentiable abstract interpretation and introduces two novel concepts: ... More Using Structured Input and Modularity for Improved LearningMar 29 2019We describe a method for utilizing the known structure of input data to make learning more efficient. Our work is in the domain of programming languages, and we use deep neural networks to do program analysis. Computer programs include a lot of structural ... More Proving Differential Privacy with Shadow ExecutionMar 28 2019Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness -- generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those ... More Generalized Convolution and Efficient Language RecognitionMar 26 2019Convolution is a broadly useful operation with applications including signal processing, machine learning, probability, optics, polynomial multiplication, and efficient parsing. Usually, however, this operation is understood and implemented in more specialized ... More Active-Code Replacement in the OODIDA Data Analytics PlatformMar 22 2019OODIDA (On-board/Off-board Distributed Data Analytics) is a platform for distributing and executing concurrent data analysis tasks. It targets a fleet of reference vehicles in the automotive industry and has a particular focus on rapid prototyping. Its ... More No more, no less - A formal model for serverless computingMar 19 2019Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. ... More Specification and Inference of Trace Refinement RelationsMar 18 2019Modern software is constantly changing. Researchers and practitioners are increasingly aware that verification tools can be impactful if they embrace change through analyses that are compositional and span program versions. Reasoning about similarities ... More Replication-Aware LinearizabilityMar 15 2019Geo-distributed systems often replicate data at multiple locations to achieve availability and performance despite network partitions. These systems must accept updates at any replica and propagate these updates asynchronously to every other replica. ... More Mutual CoinductionMar 14 2019Mar 21 2019In this paper we present mutual coinduction as a dual of mutual induction and also as a generalization of standard coinduction. In particular, we present a precise formal definition of mutual induction and mutual coinduction. In the process we present ... More Mutual CoinductionMar 14 2019Mar 19 2019In this paper we present mutual coinduction as a dual of mutual induction and as a generalization of standard coinduction. In particular, we present a formal definition of mutual induction and mutual coinduction, and in the process we present, and prove, ... More Mutual CoinductionMar 14 2019In this paper we present mutual coinduction as a dual of mutual induction and as a generalization of standard coinduction. In particular, we present a formal definition of mutual induction and mutual coinduction, and in the process we present, and prove, ... More Mutual CoinductionMar 14 2019Apr 08 2019In this paper we present mutual coinduction as a dual of mutual induction and also as a generalization of standard coinduction. In particular, we present a precise formal definition of mutual induction and mutual coinduction. In the process we present ... More SymPas: Symbolic Program SlicingMar 13 2019Program slicing is a technique for simplifying programs by focusing on selected aspects of their behaviour. Current mainstream static slicing methods operate on the PDG (program dependence graph) or SDG (system dependence graph), but these friendly graph ... More Certifying Safety when Implementing ConsensusMar 08 2019Ensuring the correctness of distributed system implementations remains a challenging and largely unaddressed problem. In this paper we present a protocol that can be used to certify the safety of consensus implementations. Our proposed protocol is efficient ... More Deductive Optimization of Relational Data StorageMar 08 2019Optimizing the physical data storage and retrieval of data are two key database management problems. In this paper, we propose a language that can express a wide range of physical database layouts, going well beyond the row- and column- based methods ... More Only Connect, SecurelyMar 07 2019The lattice model proposed by Denning in her seminal work provided secure information flow analyses with an intuitive and uniform mathematical foundation. Different organisations, however, may employ quite different security lattices. In this paper, we ... More Lenses and LearnersMar 05 2019Lenses are a well-established structure for modelling bidirectional transformations, such as the interactions between a database and a view of it. Lenses may be symmetric or asymmetric, and may be composed, forming the morphisms of a monoidal category. ... More Custom Code Generation for a Graph DSLMar 05 2019Graph algorithms are at the heart of several applications, and achieving high performance with them has become critical due to the tremendous growth of irregular data. However, irregular algorithms are quite challenging to parallelize automatically, due ... More Dijkstra Monads for AllMar 04 2019This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational ... More Oxide: The Essence of RustMar 03 2019Rust is a major advancement in industrial programming languages due in large part to its success in bridging the gap between low-level systems programming and high-level application programming. This success has ultimately empowered programmers to more ... More Induction, Coinduction, and Fixed Points in PL Type TheoryFeb 26 2019Recently we presented a concise survey of the formulation of the induction and coinduction principles, and some concepts related to them, in programming languages type theory and four other mathematical disciplines. The presentation in type theory involved ... More The $C_π$-calculus: a Model for Confidential Name PassingFeb 26 2019Feb 27 2019Sharing confidential information in distributed systems is a necessity in many applications, however, it opens the problem of controlling information sharing even among trusted parties. In this paper, we present a formal model in which dissemination of ... More Iteratively Composing Statically Verified TraitsFeb 26 2019Metaprogramming is often used to programmatically generate faster specialised code when some parameters are known in advance. To use metaprogramming and SV together, we could generate code containing contracts, and such code could be checked after metaprogramming ... More A Systematic Impact Study for Fuzzer-Found Compiler BugsFeb 25 2019Despite much recent interest in randomised testing (fuzzing) of compilers, the practical impact of fuzzer-found miscompilations on real-world applications has barely been assessed. We present the first quantitative study of the tangible impact of fuzzer-found ... More A Systematic Impact Study for Fuzzer-Found Compiler BugsFeb 25 2019Apr 08 2019Despite much recent interest in compiler fuzzing, the practical impact of fuzzer-found miscompilations on real-world applications has barely been assessed. We present the first quantitative and qualitative study of the tangible impact of fuzzer-found ... More Neural Reverse Engineering of Stripped BinariesFeb 25 2019We address the problem of predicting procedure names in stripped executables which contain no debug information. Predicting procedure names can dramatically ease the task of reverse engineering, saving precious time and human effort. We present a novel ... More Mitigating Power Side Channels during CompilationFeb 25 2019The code generation modules inside modern compilers such as GCC and LLVM, which use a limited number of CPU registers to store a large number of program variables, may introduce side-channel leaks even in software equipped with state-of-the-art countermeasures. ... More Optimizing Space of Parallel ProcessesFeb 22 2019This paper is a contribution to exploring and analyzing space-improvements in concurrent programming languages, in particular in the functional process-calculus CHF. Space-improvements are defined as a generalization of the corresponding notion in deterministic ... More