Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
The original server operated by the Mastodon gGmbH non-profit

Administered by:

Server stats:

330K
active users

mastodon.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0-nightly.2025-04-15

#rocq

0 posts0 participants0 posts today
Public
もく

discourse.rocq-prover.org/t/co

This is the saddest Discourse post I've ever read😢
#Coq -> #Rocq

Rocq Prover · Coq Community Survey 2022 Results: Part IV and ITP paper announcementCoq Community Survey 2022 Results: Part IV and ITP paper announcement TL;DR: This post completes a series of three previous posts (part I, part II, part III) with plots of answers to questions not yet analyzed in previous posts, and with the announcement of an article at ITP about the survey and the associated dataset. The Coq Community Survey 2022 was organized by an ad hoc working group and conducted during February 2022. It contained 109 questions (in English and Chinese) and received 466 an...
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
Erik Martin-Dorel

Dear Coq/ProofGeneral users,

The emacs (melpa) package of ProofGeneral has been updated to support @RocqProver 9.0.0, with or without the new CLI, so we would encourage gentle testers to give it a try. Bug reports welcome!

cf. discourse.rocq-prover.org/t/lo
and github.com/ProofGeneral/PG/iss

Rocq Prover · Looking for testers for ProofGeneral + coq9 (+ rocq cli)Dear Coq users and more specifically ProofGeneral users. The emacs (melpa) package of ProofGeneral (and the corresponding github master branch has been updated to support rocq-9 with or without the new CLI. It is probably still a bit rough on the edges and we would encourage gentle testers to give it a try. Note that Rocq is still named “Coq” everywhere in PG and it is not clear this will change soon for technical reasons. Bug reports welcome!
#rocq#rocq_prover#ProofGeneral
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 logo
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 *
Jesper Agdakx 🔸

As part of our (@sarantja@mastodon.social and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.

We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.

Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS

You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).

P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.

tudelft.fra1.qualtrics.comType-Driven Development in PracticeUnderstanding the usage and state of tools and languages for Type-Driven Development
#Agda#Coq#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 logo
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 logo
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.
ExploreLive feeds
About