编程语言
Algorithms are ways of mapping problems to solutions. An algorithm is invertible precisely when this mapping is injective, such that the initial problem can be uniquely inferred from its solution. While invertible algorithms can be…
When the inverse of an algorithm is well-defined -- that is, when its output can be deterministically transformed into the input producing it -- we say that the algorithm is invertible. While one can describe an invertible algorithm using a…
Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution, interpretation can be initially used. But after a while,…
We looked at three different object-oriented program verifiers: Gobra, KeY, and Dafny. We show that all three can be made to prove false by using a simple trick with ghost variable declaration and non-terminating code. This shows that…
We present a simple programming language based on G\"odel numbering and prime factorization, enhanced with explicit, scoped loops, allowing for easy program composition. Further, we will present a theorem prover that allows expressing and…
Automatic differentiation (AD) is conventionally understood as a family of distinct algorithms, rooted in two "modes" -- forward and reverse -- which are typically presented (and implemented) separately. Can there be only one? Following up…
Many calculi exist for modelling various features of object-oriented languages. Many of them are based on $\lambda$-calculus and focus either on statically typed class-based languages or dynamic prototype-based languages. We formalize…
Programs admitting a polyhedral representation can be transformed in many ways for locality and parallelism, notably loop tiling. Data flow analysis can then compute dependence relations between iterations and between tiles. When tiling is…
This paper presents the first machine-checked proof of noninterference for a language with gradual information-flow control, thereby establishing a rock solid foundation for secure programming languages that give programmers the choice…
Distributed protocols are generally parametric and can be executed on a system with any number of nodes, and hence proving their correctness becomes an infinite state verification problem. The most popular approach for verifying distributed…
We present the stream processing library that achieves the highest performance of existing OCaml streaming libraries, attaining the speed and memory efficiency of hand-written state machines. It supports finite and infinite streams with the…
To put static program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation. While providing sound analysis results, abstract interpretation in general can be quite costly. To…
Data types and codata types are, as the names suggest, often seen as duals of each other. However, most programming languages do not support both of them in their full generality, or if they do, they are still seen as distinct constructs…
Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. We observe that a significant class of compression methods, based on asymmetric numeral systems…
Motivated by the fast adoption of WebAssembly, we propose the first functional pipeline to support the superoptimization of WebAssembly bytecode. Our pipeline works over LLVM and Souper. We evaluate our superoptimization pipeline with 12…
String matching is a fundamental problem in algorithm. This study examines the development and construction of two reversible string-matching algorithms: a naive string-matching algorithm and the Rabin-Karp algorithm. The algorithms are…
State-of-the-art Datalog engines include expressive features such as ADTs (structured heap values), stratified aggregation and negation, various primitive operations, and the opportunity for further extension using FFIs. Current…
These proceedings include selected papers presented at the 9th Workshop on Horn Clauses for Verification and Synthesis and the Tenth International Workshop on Verification and Program Transformation, both affiliated with ETAPS 2022. Many…
Tensor algebra is essential for data-intensive workloads in various computational domains. Computational scientists face a trade-off between the specialization degree provided by dense tensor algebra and the algorithmic efficiency that…
This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in…