4 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…