-
On Algebraic Abstractions for Concurrent Separation Logics
Authors:
František Farka,
Aleksandar Nanevski,
Anindya Banerjee,
Germán Andrés Delbianco,
Ignacio Fábregas
Abstract:
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the algebraic considerations. This paper provides…
▽ More
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the algebraic considerations. This paper provides an algebraic formalization of ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations. Morphisms of structures are a standard concept in algebra and category theory, but haven't seen ubiquitous use in separation logic before. Separating relations are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads' states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.
△ Less
Submitted 4 March, 2021; v1 submitted 23 October, 2020;
originally announced October 2020.
-
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Authors:
František Farka,
Ekaterina Komendantskya,
Kevin Hammond
Abstract:
First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose…
▽ More
First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method. The paper is under consideration for acceptance in TPLP.
△ Less
Submitted 30 April, 2018;
originally announced April 2018.
-
CoALP-Ty'16
Authors:
Ekaterina Komendantskaya,
František Farka
Abstract:
This volume constitutes the pre-proceedings of the Workshop on Coalgebra, Horn Clause Logic Programming and Types (CoALP-Ty'16), held on 28--29 November 2016 in Edinburgh as a mark of the end of the EPSRC Grant Coalgebraic Logic Programming for Type Inference, by E. Komendantskaya and J. Power. This volume consists of extended abstracts describing current research in the following areas:
Semanti…
▽ More
This volume constitutes the pre-proceedings of the Workshop on Coalgebra, Horn Clause Logic Programming and Types (CoALP-Ty'16), held on 28--29 November 2016 in Edinburgh as a mark of the end of the EPSRC Grant Coalgebraic Logic Programming for Type Inference, by E. Komendantskaya and J. Power. This volume consists of extended abstracts describing current research in the following areas:
Semantics: Lawvere theories and Coalgebra in Logic and Functional Programming
Programming languages: Horn Clause Logic for Type Inference in Functional Languages and Beyond
After discussion at the workshop authors of the extended abstracts will be invited to submit a full paper to go through a second round of refereeing and selection for the formal proceedings.
△ Less
Submitted 9 December, 2016;
originally announced December 2016.
-
Coinductive Soundness of Corecursive Type Class Resolution
Authors:
František Farka,
Ekaterina Komendantskaya,
Kevin Hammond
Abstract:
Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not termi- nate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively so…
▽ More
Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not termi- nate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are induc- tively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.
△ Less
Submitted 8 December, 2016; v1 submitted 18 August, 2016;
originally announced August 2016.
