Programming Languages
Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations,…
This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher order functions and…
In this paper, we propose an explicit, non-strict representation of search trees in constraint-logic object-oriented programming. Our search tree representation includes both the non-deterministic and deterministic behaviour during…
Programmers often add meaningful information about program semantics when naming program entities such as variables, functions, and macros. However, static analysis tools typically discount this information when they look for bugs in a…
Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a…
A long-standing shortcoming of statically typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types distinguish different values of datatypes; if a program…
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following…
We present Zoea Visual which is a visual programming language based on the Zoea composable inductive programming language. Zoea Visual allows users to create software directly from a specification that resembles a set of functional test…
Component-based development is challenging in a distributed setting, for starters considering programming a task may involve the assembly of loosely-coupled remote components. In order for the task to be fulfilled, the supporting…
We present a formal study of semantics for the relational programming language miniKanren. First, we formulate a denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present…
This volume contains the proceedings of ICE'20, the 13th Interaction and Concurrency Experience, which was held online on the 19th of June 2020, as a satellite event of DisCoTec'20. The ICE workshop series features a distinguishing review…
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $\lambda$-calculus. It is derived using Danvy et al.'s functional correspondence from Cr\'egut's KN by: (1) deconstructing KN to…
Scientists construct and analyze computational models to understand the world. That understanding comes from efforts to augment, combine, and compare models of related phenomena. We propose SemanticModels.jl, a system that leverages…
With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing…
Practical adoption of static analysis often requires trading precision for performance. This paper focuses on improving the memory efficiency of abstract interpretation without sacrificing precision or time efficiency. Computationally,…
Repeated recursion unfolding is a new approach that repeatedly unfolds a recursion with itself and simplifies it while keeping all unfolded rules. Each unfolding doubles the number of recursive steps covered. This reduces the number of…
Static program analysis tools are often required to work with only a small part of a program's source code, either due to the unavailability of the entire program or the lack of need to analyze the complete code. This makes it challenging…
We propose CheckDP, the first automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample…
Recent work introduces zkay, a system for specifying and enforcing data privacy in smart contracts. While the original prototype implementation of zkay (v0.1) demonstrates the feasibility of the approach, its proof-of-concept implementation…
Mapping programs from one architecture to another plays a key role in technologies such as binary translation, decompilation, emulation, virtualization, and application migration. Although multicore architectures are ubiquitous, the…