LINCX: A Linear Logical Framework with First-Class Contexts
Abstract elided by the publisher.
26,098 papers · page 462 of 1,305
APLicative Programming with Naperian Functors
Abstract elided by the publisher.
Verified Characteristic Formulae for CakeML
Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). Th…
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a w…
Proving Linearizability Using Partial Orders
Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization --- a linear order on operations satisfying the data structure's sequential specification. Proving l…
The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with explicit non-deterministic choice. Cons-freeness roughly means that data constructors…
The Essence of Higher-Order Concurrent Separation Logic
Concurrent separation logics (CSLs) have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids (PCMs) an…
Comprehending Isabelle/HOL's Consistency
The proof assistant Isabelle/HOL is based on an extension of Higher-Order Logic HOL with ad hoc overloading of constants. It turns out that the interaction between the standard HOL type definitions and the Isabelle-specific ad hoc overloading is problematic for the logical consis…
Probabilistic Termination by Monadic Affine Sized Typing
We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out t…
The Essence of Functional Programming on Semantic Data
Abstract elided by the publisher.
A Classical Sequent Calculus with Dependent Types
Abstract elided by the publisher.
Context-Free Session Type Inference
Abstract elided by the publisher.
Modular Verification of Higher-Order Functional Programs
Abstract elided by the publisher.
Commutative Semantics for Probabilistic Programming
Abstract elided by the publisher.
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Abstract elided by the publisher.
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing log…
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Abstract elided by the publisher.
Abstract Specifications for Concurrent Maps
Abstract elided by the publisher.
Four languages and lots of macros: analyzing autotools build systems
Build systems are crucial for software system development, however there is a lack of tool support to help with their high maintenance overhead. GNU Autotools are widely used in the open source community, but users face various challenges from its hard to comprehend nature and st…