编程语言
Persistent memory (PM) is an emerging class of storage technology that combines the benefits of DRAM and SSD. This characteristic inspires research on persistent objects in PM with fine-grained concurrency control. Among such objects,…
Contextual refinement (CR) is one of the standard notions of specifying open programs. CR has two main advantages: (i) (horizontal and vertical) compositionality that allows us to decompose a large contextual refinement into many smaller…
Both logic programming in general, and Prolog in particular, have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50…
We introduce a code generator that converts unoptimized C++ code operating on sparse data into vectorized and parallel CPU or GPU kernels. Our approach unrolls the computation into a massive expression graph, performs redundant expression…
We propose a sound and complete proof rule ProbTA for quantitative analysis of violation probability of probabilistic programs. Our approach extends the technique of trace abstraction with probability in the control-flow randomness style,…
Algebraic effect handlers is a programming paradigm where programmers can declare their own syntactic operations, and modularly define the semantics of these using effect handlers. However, we cannot directly define algebraic effect…
miniKanren is a lightweight embedded language for logic and relational programming. Many of its useful features come from a distinctive search strategy, called interleaving search. However, with interleaving search conventional ways of…
System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction.…
"A generator is a parser of randomness." This perspective on generators for random data structures is well established as folklore in the programming languages community, but it has apparently never been formalized, nor have its…
Recent work has shown that Just-In-Time (JIT) compilation can introduce timing side-channels to constant-time programs, which would otherwise be a principled and effective means to counter timing attacks. In this paper, we propose a novel…
Term Rewriting Systems (TRSs) are used in compilers to simplify and prove expressions. State-of-the-art TRSs in compilers use a greedy algorithm that applies a set of rewriting rules in a predefined order (where some of the rules are not…
It is well-known that big-step semantics is not able to distinguish stuck and non-terminating computations. This is a strong limitation as it makes very difficult to reason about properties involving infinite computations, such as type…
Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to…
We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is derived by solving a suitable domain equation in the…
We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capturesome programming patterns used in untyped languages. Although occurrence typing was tied from its inceptionto set-theoretic…
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high…
This paper presents a lightweight formalism (a trace) to model message-passing concurrent executions where some common common problems can be identified, like lost or delayed messages, some forms of deadlock, etc. In particular, we consider…
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction,…
We present a technique for applying (forward and) reverse-mode automatic differentiation (AD) on a non-recursive second-order functional array language that supports nested parallelism and is primarily aimed at efficient GPU execution. The…
Context: It is common for programming languages that their reference implementation is implemented in the language itself. This requires a "bootstrap": a copy of a previous version of the implementation is provided along with the sources,…