编程语言
The objective is to demonstrate the making of Ada software available to Python and Julia programmers using GPRbuild. GPRbuild is the project manager of the GNAT toolchain. With GPRbuild the making of shared object files is fully automated…
Compiler optimization decisions are often based on hand-crafted heuristics centered around a few established benchmark suites. Alternatively, they can be learned from feature and performance data produced during compilation. However,…
Context: Gradually-typed languages allow typed and untyped code to interoperate, but typically come with significant drawbacks. In some languages, the types are unreliable; in others, communication across type boundaries can be extremely…
Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a simply-typed dialect of Prolog we call T-Prolog. The crux of…
Gate-based quantum programming languages are ubiquitous but measurement-based languages currently exist only on paper. This work introduces MCBeth, a quantum programming language which allows programmers to directly represent, program, and…
Structured recursion schemes have been widely used in constructing, optimising, and reasoning about programs over inductive and coinductive datatypes. Their plain forms, catamorphisms and anamorphisms, are restricted in expressiveness. Thus…
In machine learning (ML), researchers and engineers seem to be at odds. System implementers would prefer models to be declarative, with detailed type information and semantic restrictions that allow models to be optimised, rearranged and…
Abstract Interpretation approximates the semantics of a program by mimicking its concrete fixpoint computation on an abstract domain $\mathbb{A}$. The abstract (post-) fixpoint computation is classically divided into two phases: the…
Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities,…
Verification of C++ programs has seen considerable progress in several areas, but not for programs that use these languages' mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the…
Featherweight Go (FG) is a minimal core calculus that includes essential Go features such as overloaded methods and interface types. The most straightforward semantic description of the dynamic behavior of FG programs is to resolve method…
This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022). The meeting took place on the 2nd of April as a satellite of European Joint Conferences on Theory & Practice of…
Reversible debugging is becoming increasingly popular for locating the source of errors. This technique proposes a more natural approach to debugging, where one can explore a computation from the observable misbehaviour backwards to the…
This work explores an unexpected application of Implicit Computational Complexity (ICC) to parallelize loops in imperative programs. Thanks to a lightweight dependency analysis, our algorithm allows splitting a loop into multiple loops that…
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures -- version-space algebras,…
Rust is a young programming language gaining increased attention from software developers since it was introduced to the world by Mozilla in 2010. In this study, we attempt to answer several research questions. Does Rust deserve such…
We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and equational reasoning are mediated by the use of contextual…
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for…
Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to program such switches. The increase in speed and…
A novel model of reversible computing, the $\aleph$-calculus, is introduced. It is declarative, reversible-Turing complete, and has a local term-rewriting semantics. Unlike previously demonstrated reversible term-rewriting systems, it does…