Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
veganism.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Veganism Social is a welcoming space on the internet for vegans to connect and engage with the broader decentralized social media community.

Administered by:

Server stats:

202
active users

veganism.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0-alpha.4

#rocq

0 posts0 participants0 posts today
Public *
Jesper Agdakx 🔸
With the NWO XL consortium on Cyclic Structures in Programs and Proofs, we are looking for 6 highly motivated and talented PhD students starting in September (with some flexibility).

The topics range from Modal logic, proof theory, and coalgebras to Programming languages, concurrency, and type systems and Proof assistants (#Agda, #Rocq).

Information about the positions and application procedure can be found on the website:

cyclic-structures.gitlab.io/vacancies/

Applications will be evaluated on a rolling basis but should be submitted by the 23rd of May for full consideration.

Please forward to any strong candidates you know!

#TypeTheory #ModalLogic #Concurrency #ProgrammingLanguages #TypeSystems #ProofAssistants #CyclicStructures #PhD #Netherlands #UniversityOfGroningen #LeidenUniversity #UniversityOfTwente #TUDelft #RadboudUniversity
Cyclic Structures in Programs and ProofsVacanciesBy Jorge Perez
#radbouduniversity
Public
José A. Alonso

Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. arxiv.org/abs/2503.17159 #ITP #Coq #Rocq #Logic

arXiv.orgBi-intuitionistic logics through the abstract algebraic logic lensSince the discovery of critical mistakes in Rauszer's work on bi-intuitionistic logics, solid foundations for these have progressively been rebuilt. However, the algebraic treatment of these logics has not yet been tended to. We fill this gap by algebraically analysing the bi-intuitionistic logics wBIL and sBIL. Given that these logics are only distinguished as consequence relations, and not as sets of theorems (hence the conflation in Rauszer's work), the algebraic tools we use are tailored to the treatment of such relations. We mainly inspect these logics through the lens of abstract algebraic logic, but we also provide an alternative algebraic analysis of wBIL and sBIL as logic preserving degrees of truth and truth, respectively. Our results pertaining to wBIL and sBIL are formalised in the interactive theorem prover Rocq.
Public
José A. Alonso

MiniF2F in Rocq: Automatic translation between proof assistants (a case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesúss Gallego Arias, Marc Lelarge. arxiv.org/abs/2503.04763 #LLMs #Rocq #LeanProver #IsabelleHOL #Math

arXiv.orgMiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case StudyIn this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that incorporate feedback from unsuccessful attempts. At each stage, we perform multiple rounds of translation using increasingly advanced models: GPT-4o mini, Claude 3.5 Sonnet, o1 mini, and o1. We successfully translated 478 out of 488 theorems. The dataset is opensource: https://github.com/LLM4Rocq/miniF2F-rocq.
Public
José A. Alonso

Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. arxiv.org/abs/2502.21156 #ITP #Coq #Rocq

arXiv.orgCryptis: Cryptographic Reasoning in Separation LogicWe introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq.
Public
José A. Alonso

Strands Rocq: Why is a security protocol correct, mechanically? ~ Matteo Busi, Riccardo Focardi, Flaminia L. Luccio. arxiv.org/abs/2502.12848 #ITP #Rocq #Coq

arXiv.orgStrands Rocq: Why is a Security Protocol Correct, Mechanically?Strand spaces are a formal framework for symbolic protocol verification that allows for pen-and-paper proofs of security. While extremely insightful, pen-and-paper proofs are error-prone, and it is hard to gain confidence on their correctness. To overcome this problem, we developed StrandsRocq, a full mechanization of the strand spaces in Coq (soon to be renamed Rocq). The mechanization was designed to be faithful to the original pen-and-paper development, and it was engineered to be modular and extensible. StrandsRocq incorporates new original proof techniques, a novel notion of maximal penetrator that enables protocol compositionality, and a set of Coq tactics tailored to the domain, facilitating proof automation and reuse, and simplifying the work of protocol analysts. To demonstrate the versatility of our approach, we modelled and analyzed a family of authentication protocols, drawing inspiration from ISO/IEC 9798-2 two-pass authentication, the classical Needham-Schroeder-Lowe protocol, as well as a recently-proposed static analysis for a key management API. The analyses in StrandsRocq confirmed the high degree of proof reuse, and enabled us to distill the minimal requirements for protocol security. Through mechanization, we identified and addressed several issues in the original proofs and we were able to significantly improve the precision of the static analysis for the key management API. Moreover, we were able to leverage the novel notion of maximal penetrator to provide a compositional proof of security for two simple authentication protocols.
VegansExploreLive feeds
About