Programming Languages
Most existed work require knowledge about the effect of program instructions (or statements) to analyze and verify algorithms. In this paper, by revealing some findings on executions of object programs, we define two basic concepts --…
We present an approach for a lightweight datatype-generic programming in Objective Caml programming language aimed at better code reuse. We show, that a large class of transformations usually expressed via recursive functions with pattern…
In the last years Node.js has emerged as a framework particularly suitable for implementing lightweight IoT applications, thanks to its underlying asynchronous event-driven, non blocking I/O model. However, verifying the correctness of…
Verification of functional correctness of control programs is an essential task for the development of space electronics; it is difficult and time-consuming and typically outweighs design and programming tasks in terms of development hours.…
Rascal is a high-level transformation language that aims to simplify software language engineering tasks like defining program syntax, analyzing and transforming programs, and performing code generation. The language provides several…
A demand-driven approach to program analysis have been viewed as efficient algorithms to compute only the information required to serve a target demand. In contrast, an exhaustive approach computes all information in anticipation of it…
Deep learning software demands reliability and performance. However, many of the existing deep learning frameworks are software libraries that act as an unsafe DSL in Python and a computation graph interpreter. We present DLVM, a design and…
We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally…
This paper studies two variants of tiling: iteration space tiling (or loop blocking) and cache-oblivious methods that recursively split the iteration space with divide-and-conquer. The key question to answer is when we should be using one…
Grammar-based sentence generation has been thoroughly explored for Context-Free Grammars (CFGs), but remains unsolved for recognition-based approaches such as Parsing Expression Grammars (PEGs). Lacking tool support, language designers…
We consider the task of analyzing message-passing programs by observing their run-time behavior. We introduce a purely library-based instrumentation method to trace communication events during execution. A model of the dependencies among…
Flow- and context-sensitive points-to analysis is difficult to scale; for top-down approaches, the problem centers on repeated analysis of the same procedure; for bottom-up approaches, the abstractions used to represent procedure summaries…
Numerical applications and, more recently, machine learning applications rely on high-dimensional data that is typically organized into multi-dimensional tensors. Many existing frameworks, libraries, and domain-specific languages support…
In this paper, we present two new forms of the $write$ statement: one of the form $write(x);G$ where $G$ is a statement and the other of the form $write(x);D$ where $D$ is a module. The former is a generalization of traditional $write$…
This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed lambda-calculus. The proposed…
Modular programming is a cornerstone in software development, as it allows to build complex systems from the assembly of simpler components, and support reusability and substitution principles. In a distributed setting, component assembly…
We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It…
The majority of industrial-strength object-oriented (OO) software is written using nominally-typed OO programming languages. Extant domain-theoretic models of OOP developed to analyze OO type systems miss, however, a crucial feature of…
Recently, the k-induction algorithm has proven to be a successful approach for both finding bugs and proving correctness. However, since the algorithm is an incremental approach, it might waste resources trying to prove incorrect programs.…
Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type {\Omega}, the auto- autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most…