arXiv subjects

František Farka

Publications and source records attributed to František Farka.

6 recordsLinked to original sources

arXiv2026

Corten - Foundational Verification of Rust Programs

We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first semantics of surface-level Rust mechanized in a proof assistant with an attached program logic, directly grounded in the Rust Reference: it deeply embeds the Typed High-level Intermediate Representation (THIR) into Rocq and formalises Rust's dynamic semantics as a weakest-precondition predicate transformer calculus. By operating at THIR rather than on internal compiler representations, Corten proof goals display the THIR AST, which pretty-prints to surface Rust, keeping verification close to the source code and facilitating maintainability as code evolves. Atop this semantics, Corten develops a program logic and a syntax-directed proof automation layer; the program logic includes defunctionalized continuation stacks that keep proof goals first-order and compact. Soundness is established incrementally, construct by construct, against an interaction-trees denotation. A synthetic test suite demonstrates a two-to-four times reduction in proof size compared to raw semantic proofs. We further showcase Corten on a buddy allocator case study, verifying memory safety of the allocation and deallocation functions, laying the groundwork for end-to-end verification in a shared Rocq semantic foundation spanning hardware-software boundaries.

cs.PL↗

arXiv2026

NoC-Out: A Formally-verified Network-on-Chip Library for Rule-based Hardware Designs

The Network-on-Chip (NoC) is the communication backbone of any multiprocessor chip. A failure of the NoC has severe consequences for the whole system. Yet, no approach exists that provides formally-verified NoCs with strong guarantees but without tedious verification effort. Any library that generates formally-verified NoCs needs to be parametric in the structure of the NoC. This requires a hardware description language (HDL) that allows for parametric and concurrent yet efficient hardware designs as well as the necessary program logic to reason about them in a modular fashion. So far, HDLs fall short in both aspects. In this paper, we implement NoC-Out, the first library/generator for formally-verified k-dimensional NoC designs. In order to build NoC-Out, we extended K\^oika, a rule-based HDL in the Rocq theorem prover, with support for concurrent yet efficient NoC designs and a program logic for modular, automated reasoning. Given a configuration, NoC-Out produces a k-dimensional torus NoC in K\^oika, which can then be compiled to Verilog. Each produced NoC is equipped with a proof that it refines our formal NoC specification; no additional verification effort is required. Our specification proves a strong liveness guarantee, which consequently applies to all generated NoCs. In our evaluation, we find that our verification approach is even required to synthesize efficient NoCs in rule-based HDLs.

cs.PL↗

arXiv2020

On Algebraic Abstractions for Concurrent Separation Logics

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.

cs.PL↗

arXiv2018

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

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.

cs.LO↗

arXiv2016

CoALP-Ty'16

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.

cs.LO↗

arXiv2016

Coinductive Soundness of Corecursive Type Class Resolution

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.

cs.PL↗