Programming Languages
Over the past decade, reactive frameworks and languages have become the dominant programming paradigm in front-end web development. In this paradigm, user actions change application state, and those changes propagate reactively to derived…
We present a statically typed embedding of relational programming (specifically a dialect of miniKanren with disequality constraints) in Haskell. Apart from handling types, our dialect extends standard relational combinator repertoire with…
Session types using affinity and exception handling mechanisms have been developed to ensure the communication safety of protocols implemented in concurrent and distributed programming languages. Nevertheless, current affine session types…
Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such…
We integrate integrity constraints to stableKanren to enable a new problem-solving paradigm in combinatorial search problems. stableKanren extends miniKanren to reasoning about contradictions under stable model semantics. However, writing…
This paper explores options for implementing the relation $n \equiv 0 \ (\text{mod} \ 3)$ within miniKanren using miniKanren numbers and its arithmetic suite. We examine different approaches starting from straightforward implementations to…
We improve the backward compatibility of stableKanren to run miniKanren programs. stableKanren is a miniKanren extension capable of non-monotonic reasoning through stable model semantics. However, standard miniKanren programs that produce…
Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loaded code, concurrent code, and language properties. Existing…
In top-down enumeration for program synthesis, abstraction-based pruning uses an abstract domain to approximate the set of possible values that a partial program, when completed, can output on a given input. If the set does not contain the…
We are currently developing an innovative and visually-driven programming language called Omega.Although the Omega code is stored in text files, these files are not intended for manual editing or traditional printing.Furthermore, parsing…
Compilers convert between representations -- usually, from higher-level, human writable code to lower-level, machine-readable code. A compiler backend is the portion of the compiler containing optimizations and code generation routines for…
Suppose we are given two OCaml modules implementing the same signature. How do we check that they are observationally equivalent -- that is, that they behave the same on all inputs? One established technique is to use a property-based…
Deep R Programming is a comprehensive and in-depth introductory course on one of the most popular languages for data science. It equips ambitious students, professionals, and researchers with the knowledge and skills to become independent…
Design of an efficient thread-safe concurrent data structure is a balancing act between its implementation complexity and performance. Lock-based concurrent data structures, which are relatively easy to derive from their sequential…
With the growing sizes of data structures allocated in heap, understanding the actual use of heap memory is critically important for minimizing cache misses and reclaiming unused memory. A static analysis aimed at this is difficult because…
ReScript introduces a strongly typed language that targets JavaScript, as an alternative to gradually typed languages, such as TypeScript. In this paper, we present a type system for data-flow analysis for a subset of the ReScript language,…
Computational interpretations of linear logic allow static control of memory resources: the data produced by the program are endowed through its type with attributes that determine its life cycle. This has promoted numerous investigations…
Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step-indexing comes, however,…
Software developers must adapt to keep up with the changing capabilities of platforms so that they can utilize the power of High- Performance Computers (HPC), including exascale systems. OpenMP, a directive-based parallel programming model,…
Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow to remove certain paradoxes…