26,098 papers · page 110 of 1,305
Abstract Equality is at the heart of dependent type theory, as it plays a fundamental role in specifications and mathematical reasoning. The standard way to handle it in mainstream proof assistants such as Agda, Lean or Coq is based on Martin-Löf’s identity type, which comes stra…
Abstract Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of byte-addressable persistent memory, a natural question to ask is whether STM systems can be …
Abstract This report extends §6 of the main paper by providing further details of the mechanisation effort.
Abstract We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correct…
Abstract Invertible programming languages specify transformations to be run in two directions, such as compression/decompression or encryption/decryption. Two key concepts in invertible programming languages are partial invertibility and local invertibility. Partial invertibility…
Design by Contract represents an established, lightweight paradigm for engineering reliable and robust software systems by specifying verifiable expectations and obligations between software components. Due to its laborious nature, developers hardly adopt Design by Contract in pr…
We propose DDLoader, a system that embeds information about data partitioning and data distribution in distributed file systems using a metaprogramming framework. We demonstrate that this technique has practical benefits for building applications that interact with distributed fi…
Giving auto-completion candidates for dynamically typed languages requires complex analysis of the source code, especially when the goal is to ensure that the completion candidates do not introduce bugs. In this paper, we introduce an approach that builds upon abstract interpreta…
Practical metaprogramming applications often involve manipulating open code fragments, which is easy to get wrong in the absence of static verification that all variable occurrences remain correctly bound. Many approaches have been proposed to verify the type- and scope-safety of…
When applying model-driven engineering in an agile environment, new requirements continuously expand the domain scope and trigger an extension of the concepts covered by the Domain-Specific Language (DSL). While programming languages streamline code extension and reuse through li…
Assessing code quality is crucial for effective software maintenance and evolution. Traditional tools like SonarQube offer valuable insights at the application level but lack the granularity needed for detailed, feature-specific analysis. This paper emphasizes the importance of f…
Inlining is a well-studied compiler transformation that can reduce call overhead and enable further optimizations. As functional programming languages such as Haskell have functions as first-class objects, they potentially have the most to gain from inlining. However, despite bei…
Staged computation is a means to achieve maintainability and high performance simultaneously, by allowing a programmer to express domain-specific optimizations in a high-level programming language. Multi-stage programming languages such as MetaOCaml provide a static safety guaran…
In recent years, Datalog has sparked renewed interest in academia and industry, leading to the development of numerous new Datalog systems. To unify these systems, recent approaches treat Datalog as an intermediate representation (IR) in a compiler framework: Compiler frontends c…
This paper addresses the complexity of developing optimizing compilers by proposing a novel design pattern named Restage. The Restage interface reduces boilerplate code in transformation passes by simplifying the extraction and reconstruction of language constructs, thereby enabl…
MicroHs is a compiler for Haskell2010. It translates Haskell to SKI style combinators via λ-calculus. The runtime system is quite small with few dependencies.
Formal reasoning about the time complexity of algorithms and data structures is usually done in interactive theorem provers like Isabelle/HOL. This includes reasoning about amortized time complexity which looks at the worst case performance over a series of operations. However, m…
Despite the intended use for prototyping or as a first step towards giving semantics to a new programming language, interpreters are often monolithic and difficult to extend. Higher-order effects and handlers promise modular composition of handlers and semantics; in practice, how…
Much work in the area of compiler calculation has focused on pure languages. While this simplifies the reasoning, it reduces the applicability. In this article, we show how an existing compiler calculation methodology can be naturally extended to languages with side effects. We a…
At present, the most efficient implementations of Arrowized Functional Reactive Programming (AFRP), such as Scalable FRP (SFRP), do not support the loop combinator. This prevents us from expressing fundamental programs in such implementations, which limits AFRP’s use in domains w…