7 citations · 9 across the 6 of their papers we have counts for
6 papers
Corten - Foundational Verification of Rust Programs
František Farka, Carmine Abate, Sven Linker +1
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 seman…
Dataset Scarcity Limits Robust Evaluation of Multilingual Embedding Models: A Case Study of Slavic Languages
Ana Gjorgjevikj, Barbara Koroušić Seljak, Tome Eftimov
Multilingual text embedding models enable cross-lingual transfer of knowledge across a wide range of NLP tasks, but their evaluation remains highly uneven across high-, mid- and lo…
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee +2
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that…
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
František Farka, Ekaterina Komendantskya, Kevin Hammond
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…
CoALP-Ty'16
Ekaterina Komendantskaya, František Farka
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…
Coinductive Soundness of Corecursive Type Class Resolution
František Farka, Ekaterina Komendantskaya, Kevin Hammond
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,…