Computer Science - Programming Languages Publications (50)


Computer Science - Programming Languages Publications

We introduce a system of monadic affine sized types, which substantially generalise usual sized types, and allows this way to capture probabilistic higher-order programs which terminate almost surely. Going beyond plain, strong normalisation without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. Read More

In an algorithmic complexity attack, a malicious party takes advantage of the worst-case behavior of an algorithm to cause denial-of-service. A prominent algorithmic complexity attack is regular expression denial-of-service (ReDoS), in which the attacker exploits a vulnerable regular expression by providing a carefully-crafted input string that triggers worst-case behavior of the matching algorithm. This paper proposes a technique for automatically finding ReDoS vulnerabilities in programs. Read More

We propose Edward, a Turing-complete probabilistic programming language. Edward builds on two compositional representations---random variables and inference. By treating inference as a first class citizen, on a par with modeling, we show that probabilistic programming can be as flexible and computationally efficient as traditional deep learning. Read More

This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort. The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the system. Read More

Obtaining good performance when programming heterogeneous computing platforms poses significant challenges. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code with semantic annotations is transformed into functionally equivalent code better suited for a given platform. The transformation steps are represented as rules that can be fired when certain syntactic and semantic conditions are fulfilled. Read More

This volume contains a selection of the papers presented at the XVI Jornadas sobre Programaci\'on y Lenguajes (PROLE 2016), held at Salamanca, Spain, during September 14th-15th, 2016. Previous editions of the workshop were held in Santander (2015), C\'adiz (2014), Madrid (2013), Almer\'ia (2012), A Coru\~na (2011), Val\`encia (2010), San Sebasti\'an (2009), Gij\'on (2008), Zaragoza (2007), Sitges (2006), Granada (2005), M\'alaga (2004), Alicante (2003), El Escorial (2002), and Almagro (2001). Programming languages provide a conceptual framework which is necessary for the development, analysis, optimization and understanding of programs and programming tasks. Read More

We study the termination problem for nondeterministic recursive probabilistic programs. First, we show that a ranking-supermartingales-based approach is both sound and complete for bounded terminiation (i.e. Read More

Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes. Existing type systems for datasort refinements require that all the refinements of a type be specified when the type is declared; multiple refinements of the same type can be obtained only by duplicating type definitions, and consequently, duplicating code. Read More

A devil's advocate is one who argues against a claim, not as a committed opponent but in order to determine the validity of the claim. We are interested in a devil's advocate that argues against termination of a program. He does so by producing a maleficent program that can cause the non-termination of the original program. Read More

Constraint Handling Rules (CHR) is both an effective concurrent declarative constraint-based programming language and a versatile computational formalism. While conceptually simple, CHR is distinguished by a remarkable combination of desirable features: - semantic foundation in classical and linear logic, - effective and efficient sequential and parallel execution model - guaranteed properties like the anytime online algorithm properties - powerful analysis methods for deciding essential program properties. This overview of CHR research and applications is by no complete. Read More

This paper is concerned with rule-based programs that go wrong. The unwanted behavior of rule applications is non-termination or failure of a computation. We propose a static program analysis of the non-termination problem for recursion in the Constraint Handling Rules (CHR) language. Read More

Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory cannot support higher-order functions, that is, the category of measurable spaces is not cartesian closed. Read More

In recent years, Deep Learning (DL) has found great success in domains such as multimedia understanding. However, the complex nature of multimedia data makes it difficult to develop DL-based software. The state-of-the art tools, such as Caffe, TensorFlow, Torch7, and CNTK, while are successful in their applicable domains, are programming libraries with fixed user interface, internal representation, and execution environment. Read More

We propose a new concurrent model for imperative languages where concurrency occurs at a subprogram level. This model introduces a new {\it block sequential} statement of the form $#(G_1,\ldots,G_n)$ where each $G_i$ is a statement. This statement tells the machine to execute $G_1,\ldots,G_n$ sequentially and atomically (\ie, without interleaving). Read More

Affiliations: 1INRIA and LIX, École Polytechnique

The lambda-calculus is a peculiar computational model whose definition does not come with a notion of machine. Unsurprisingly, implementations of the lambda-calculus have been studied for decades. Abstract machines are implementations schema for fixed evaluation strategies that are a compromise between theory and practice: they are concrete enough to provide a notion of machine and abstract enough to avoid the many intricacies of actual implementations. Read More

Affiliations: 1Goethe-University Frankfurt, Germany, 2Goethe-University Frankfurt, Germany

We present an implementation of an interpreter LRPi for the call-by-need calculus LRP, based on a variant of Sestoft's abstract machine Mark 1, extended with an eager garbage collector. It is used as a tool for exact space usage analyses as a support for our investigations into space improvements of call-by-need calculi. Read More

Affiliations: 1Portland State University, 2CAU Kiel, 3Portland State University

We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. Read More

Paisley is an extensible lightweight embedded domain-specific language for nondeterministic pattern matching in Java. Using simple APIs and programming idioms, it brings the power of functional-logic processing of arbitrary data objects to the Java platform, without constraining the underlying object-oriented semantics. Here we present an extension to the Paisley framework that adds pattern-based control flow. Read More


We present a framework for building CLP languages with symbolic constraints based on microKanren, a domain-specific logic language shallowly embedded in Racket. We rely on Racket's macro system to generate a constraint solver and other components of the microKanren embedding. The framework itself and the constraints' implementations amounts to just over 100 lines of code. Read More

Affiliations: 1Universidad de Málaga, 2Universidad de Málaga, 3Universidad de Málaga

The Timed Concurrent Constraint Language tccp is a declarative synchronous concurrent language, particularly suitable for modelling reactive systems. In tccp, agents communicate and synchronise through a global constraint store. It supports a notion of discrete time that allows all non-blocked agents to proceed with their execution simultaneously. Read More

We present an extension of the declarative programming language Curry to support the access to data stored in relational databases via SQL. Since Curry is statically typed, our emphasis on this SQL integration is on type safety. Our extension respects the type system of Curry so that run-time errors due to ill-typed data are avoided. Read More

System relevant embedded software needs to be reliable and, therefore, well tested, especially for aerospace systems. A common technique to verify programs is the analysis of their abstract syntax tree (AST). Tree structures can be elegantly analyzed with the logic programming language Prolog. Read More


We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration if all other methods fail. An important aspect is detecting when enumeration was complete and if this has an impact on the soundness of the result. Read More

The methods to access large relational databases in a distributed system are well established: the relational query language SQL often serves as a language for data access and manipulation, and in addition public interfaces are exposed using communication protocols like REST. Similarly to REST, GraphQL is the query protocol of an application layer developed by Facebook. It provides a unified interface between the client and the server for data fetching and manipulation. Read More

Bottom-up evaluation of Datalog has been studied for a long time, and is standard material in textbooks. However, if one actually wants to develop a deductive database system, it turns out that there are many implementation options. For instance, the sequence in which rule instances are applied is not given. Read More

Modern knowledge base systems frequently need to combine a collection of databases in different formats: e.g., relational databases, XML databases, rule bases, ontologies, etc. Read More

We demonstrate a modularity bug in the interface system of Java 8 on the practical example of a textbook design of a modular interface for vector spaces. Our example originates in our teaching of modular object-oriented design in Java 8 to undergraduate students, simply following standard programming practices and mathematical definitions. The bug shows up as a compilation error and should be fixed with a language extension due to the importance of best practices (design fidelity). Read More

This volume contains the formal proceedings of the Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), held on 23rd June 2016 in Porto, Portugal, as a satellite event of the First International Conference on Formal Structures for Computation and Deduction (FSCD 2016). The workshop brought together researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. Read More

We present lifestate rules--an approach for abstracting event-driven object protocols. Developing applications against event-driven software frameworks is notoriously difficult. One reason why is that to create functioning applications, developers must know about and understand the complex protocols that abstract the internal behavior of the framework. Read More

The Workshops on (Constraint) Logic Programming (WLP) are the annual meeting of the German Society of Logic Programming (Gesellschaft f\"ur Logische Programmierung e.V., GLP) and bring together researchers interested in logic programming, constraint programming, answer set programming, and related areas like databases and artificial intelligence (not only from Germany). Read More

We present a technique for automatically generating features for data-driven program analyses. Recently data-driven approaches for building a program analysis have been proposed, which mine existing codebases and automatically learn heuristics for finding a cost-effective abstraction for a given analysis task. Such approaches reduce the burden of the analysis designers, but they do not remove it completely; they still leave the highly nontrivial task of designing so called features to the hands of the designers. Read More

Extensible variants improve the modularity and expressiveness of programming languages: they allow program functionality to be decomposed into independent blocks, and allow seamless extension of existing code with both new cases of existing data types and new operations over those data types. This paper considers three approaches to providing extensible variants in Haskell. Row typing is a long understood mechanism for typing extensible records and variants, but its adoption would require extension of Haskell's core type system. Read More

As originally proposed, type classes provide overloading and ad-hoc definition, but can still be understood (and implemented) in terms of strictly parametric calculi. This is not true of subsequent extensions of type classes. Functional dependencies and equality constraints allow the satisfiability of predicates to refine typing; this means that the interpretations of equivalent qualified types may not be interconvertible. Read More

We introduce ProjectQ, an open source software effort for quantum computing. The first release features a compiler framework capable of targeting various types of hardware, a high-performance simulator with emulation capabilities, and compiler plug-ins for circuit drawing and resource estimation. We introduce our Python-embedded domain-specific language, present the features, and provide example implementations for quantum algorithms. Read More

We present DroidGen a tool for automatic anti-malware policy inference. DroidGen employs a data-driven approach: it uses a training set of malware and benign applications and makes call to a constraint solver to generate a policy under which a maximum of malware is excluded and a maximum of benign applications is allowed. Preliminary results are encouraging. Read More

Programming a parallel computing system that consists of several thousands or even up to a million message passing processing units may ask for a language that supports waiting for and sending messages over hardware channels. As programs are looked upon as state machines, the language provides syntax to implement a main event driven loop. The language presented herewith surely will not serve as a generic programming language for any arbitrary task. Read More

Type assignment systems are known to grant or characterize normalization. The grammar of the types they feature is usually inductive. It is easy to see that, when types are coinductively generated, we obtain unsound type systems (meaning here that they are able to type some non head-normalizing terms). Read More

Stream processing is mainstream (again): Widely-used stream libraries are now available for virtually all modern OO and functional languages, from Java to C# to Scala to OCaml to Haskell. Yet expressivity and performance are still lacking. For instance, the popular, well-optimized Java 8 streams do not support the zip operator and are still an order of magnitude slower than hand-written loops. Read More

We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. Read More

Verifying multi-threaded programs is becoming more and more important, because of the strong trend to increase the number of processing units per CPU socket. We introduce a new configurable program analysis for verifying multi-threaded programs with a bounded number of threads. We present a simple and yet efficient implementation as component of the existing program-verification framework CPAchecker. Read More

Most type systems that support polymorphic functions are based on a version of System-F. We argue that this limits useful programming paradigms for languages with lazy evaluation. We motivate an extension of System-F alleviating this limitation. Read More

Affiliations: 1Saarland University, Germany, 2Saarland University, Germany

Domain-specific languages are becoming increasingly important. Almost every application touches multiple domains. But how to define, use, and combine multiple DSLs within the same application? The most common approach is to split the project along the domain boundaries into multiple pieces and files. Read More

Increasing scale and complexity of modern software, we have found programming problem with techniques like Aspect-oriented Programming(AOP) while constructing features of the software. We capture its key property as behavioral similarity, a set of tangled and scattered low-level behavior in similar patterns of invocation across the high-level behaviors - features in software. In this paper, we present Self-composable Programming(Self), a way of programming for constructing reusable software patterns. Read More

Affiliations: 1Sapienza University, 2University of Brighton, 3Sapienza University

We introduce type annotations as a flexible typing mechanism for graph systems and discuss their advantages with respect to classical typing based on graph morphisms. In this approach the type system is incorporated with the graph and elements can adapt to changes in context by changing their type annotations. We discuss some case studies in which this mechanism is relevant. Read More

Affiliations: 1Saarland University, Germany, 2Saarland University, Germany

When creating a new domain-specific language (DSL) it is common to embed it as a part of a flexible host language, rather than creating it entirely from scratch. The semantics of an embedded DSL (EDSL) is either given directly as a set of functions (shallow embedding), or an AST is constructed that is later processed (deep embedding). Typically, the deep embedding is used when the EDSL specifies domain-specific optimizations (DSO) in a form of AST transformations. Read More

The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it - in particular, general inductive types are not part of the system. Read More

Functional languages with strong static type systems have beneficial properties to help ensure program correctness and reliability. Surprisingly, their practical significance in applications is low relative to other languages lacking in those dimensions. In this paper, the programs-as-proofs analogy is taken seriously to gain speculative insights by analysis of creation habits in the proof-centric discipline of mathematics. Read More

Today's JavaScript applications are composed of scripts from different origins that are loaded at run time. As not all of these origins are equally trusted, the execution of these scripts should be isolated from one another. However, some scripts must access the application state and some may be allowed to change it, while preserving the confidentiality and integrity constraints of the application. Read More

We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades. Dynamic SOS (DSOS) is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. Read More

Known algorithms for manipulating octagons do not preserve their sparsity, leading typically to quadratic or cubic time and space complexities even if no relation among variables is known when they are all bounded. In this paper, we present new algorithms, which use and return octagons represented as weakly closed difference bound matrices, preserve the sparsity of their input and have better performance in the case their inputs are sparse. We prove that these algorithms are as precise as the known ones. Read More