Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
Abstract elided by the publisher.
26,098 papers · page 491 of 1,305
Detecting All High-Level Dataraces in an RTOS Kernel
Abstract elided by the publisher.
Reachability for Dynamic Parametric Processes
In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is deci…
Conjunctive Abstract Interpretation Using Paramodulation
Abstract elided by the publisher.
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Separation Logic (\(\mathsf {SL}\)) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order \(\mathsf {SL}\) restricted to the Bernays-Schonfinke…
Finding Relevant Templates via the Principal Component Analysis
Abstract elided by the publisher.
Sound Bit-Precise Numerical Domains
Abstract elided by the publisher.
IC3 - Flipping the E in ICE
Abstract elided by the publisher.
Interactive programming in Agda - Objects and graphical user interfaces
Abstract We develop a methodology for writing interactive and object-based programs (in the sense of Wegner) in dependently typed functional programming languages. The methodology is implemented in the ooAgda library. ooAgda provides a syntax similar to the one used in object-ori…
Normal-order reduction grammars
Abstract We present an algorithm which, for given n , generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set {S, K} of primitive combinators, requiring exactly n normal-order reduction steps to normalize. As a consequence of Curry …
Contributions to a computational theory of policy advice and avoidability
Abstract We present the starting elements of a mathematical theory of policy advice and avoidability. More specifically, we formalize a cluster of notions related to policy advice, such as policy , viability , reachability , and propose a novel approach for assisting decision mak…
Computation semantics of the functional scientific workflow language Cuneiform
Abstract Cuneiform is a minimal functional programming language for large-scale scientific data analysis. Implementing a strict black-box view on external operators and data, it allows the direct embedding of code in a variety of external languages like Python or R, provides data…
The essence of ornaments
Abstract Functional programmers from all horizons strive to use, and sometimes abuse, their favorite type system in order to capture the invariants of their programs. A widely used tool in that trade consists in defining finely indexed datatypes. Operationally, these types classi…
An algebra for distributed Big Data analytics
Abstract We present an algebra for data-intensive scalable computing based on monoid homomorphisms that consists of a small set of operations that capture most features supported by current domain-specific languages for data-centric distributed computing. This algebra is being us…
Correctness of compiling polymorphism to dynamic typing
Abstract The connection between polymorphic and dynamic typing was originally considered by Curry et al. (1972, Combinatory Logic , vol. ii) in the form of “polymorphic type assignment” for untyped λ-terms. Types are assigned after the fact to what is, in modern terminology, a dy…
PhD Abstracts
Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
PhD Abstracts
Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
Compiling a 50-year journey
Abstract Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this art…
Call-by-name extensionality and confluence
Abstract Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like η as reduction rules easily breaks confluence. We explore these issues in the se…
No value restriction is needed for algebraic effects and handlers
Abstract We present a straightforward, sound, Hindley–Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that th…