Latest in cs.pl
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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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