Erik Martin-Dorel<p>Dear Coq/ProofGeneral users,</p><p>The emacs (melpa) package of ProofGeneral has been updated to support <span class="h-card" translate="no"><a href="https://mastodon.acm.org/@RocqProver" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>RocqProver</span></a></span> 9.0.0, with or without the new CLI, so we would encourage gentle testers to give it a try. Bug reports welcome!</p><p>cf. <a href="https://discourse.rocq-prover.org/t/looking-for-testers-for-proofgeneral-coq9-rocq-cli/2590" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">discourse.rocq-prover.org/t/lo</span><span class="invisible">oking-for-testers-for-proofgeneral-coq9-rocq-cli/2590</span></a><br>and <a href="https://github.com/ProofGeneral/PG/issues" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/ProofGeneral/PG/iss</span><span class="invisible">ues</span></a></p><p><a href="https://fosstodon.org/tags/rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>rocq</span></a> <a href="https://fosstodon.org/tags/rocq_prover" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>rocq_prover</span></a> <a href="https://fosstodon.org/tags/ProofGeneral" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProofGeneral</span></a></p>
Recent searches
Search options
Administered by:
#rocq
1 post1 participant0 posts today
Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. https://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.
Qiita - 人気の記事 PHOASでshift/resetのCPS変換 in Rocq(旧Coq)
https://qiita.com/mrkbc/items/89b034dadc69df2ad274?utm_campaign=popular_items&utm_medium=feed&utm_source=popular_items
QiitaPHOASでshift/resetのCPS変換 in Rocq(旧Coq) - Qiitaこの記事は(株)proof ninjaの助成を受けて執筆しています．みなさんこんにちは．2025年3月12日，Coqが正式に名前が変わり，Rocq 9.0.0 がリリースされましたね．私はまだ慣れ…
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
MiniF2F in Rocq: Automatic translation between proof assistants (a case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesúss Gallego Arias, Marc Lelarge. https://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.
Readings shared March 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/07-readings_shared_03-07-25 #Agda #CategoryTheory #Coq #HoTT #ITP #LLMs #LeanProver #Math #Programming #Reasoning #Rocq #TypeTheory
Vestigium · Readings shared February 7, 2025The readings shared in Bluesky on 7 March 2025 are
A formalisation of addition chains. ~ Laurent Théry. #ITP #Coq #Rocq
QED in context (An observation study of proof assistant users). ~ Jessica Shi,
A formalisation of addition chains. ~ Laurent Théry. https://hal.science/hal-04971933/document #ITP #Coq #Rocq
QED in context (An observation study of proof assistant users). ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, Andrew Head.https://jwshii.github.io/OOPSLA25.pdf #ITP #LeanProver #Coq #Rocq
Readings shared March 6, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/06-readings_shared_03-06-25 #ITP #LeanProver #Coq #Rocq #LLMs
Vestigium · Readings shared February 6, 2025The readings shared in Bluesky on 6 March 2025 are
Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #Coq #Rocq
Lean-STaR: Learning to
Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. https://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.
Readings shared March 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/02-readings_shared_03-02-25 #ITP #IsabelleHOL #Coq #Rocq
Vestigium · Readings shared February 2, 2025The readings shared in Bluesky on 2 March 2025 are
Faithful logic embeddings in HOL (A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples,
BiCoq: Bigraphs formalisation with Coq. ~ Cécile Marcon et als. https://www.dcs.gla.ac.uk/~michele/papers/SAC2025.pdf #ITP #Coq #Rocq
Readings shared February 25, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/25-readings_shared_02-25-25 #Coq #ITP #LLMs #LeanProver #Logic #Math #PhDThesis #Rocq #SAT #SMT
Vestigium · Readings shared February 25, 2025The readings shared in Bluesky on 25 February 2025 are
Towards a formalized theory of solid modules. ~ Dagur Asgeirsson. #PhDThesis #ITP #LeanProver #Math
Prove your colorings: Formal verification of
Prove your colorings: Formal verification of cache coloring of Bao hypervisor. ~ Axel Ferréol, Laurent Corbin, Nikolai Kosmatov. https://www.nikolai-kosmatov.eu/publications/ferreol_ck_fase_2025.pdf #ITP #Coq #Rocq
Readings shared February 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/23-readings_shared_02-23-25 #ATP #Coq #ITP #IsabelleHOL #Mace4 #Math #Mizar #Prover9 #Rocq
Vestigium · Readings shared February 23, 2025The readings shared in Bluesky on 23 February 2025 are
Power operator for lists (in Isabelle/HOL). ~ Štěpán Holub, Martin Raška, Štěpán Starosta, Tobias Nipkow. #ITP #IsabelleHOL
Strands Rocq: Why is
Strands Rocq: Why is a security protocol correct, mechanically? ~ Matteo Busi, Riccardo Focardi, Flaminia L. Luccio. https://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.
Readings shared February 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/21-readings_shared_02-21-25 #AI #Autoformalization #Coq #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LeanProver #Math #OCaml #Rocq
Vestigium · Readings shared February 21, 2025The readings shared in Bluesky on 21 February 2025 are
Machine-assisted proofs (February 19, 2025). ~ Terence Tao. #ITP #LeanProver #AI #Math
Formalisation of combinatorial optimisation in Isabelle/H
A Coq implementation of a theory of tagged objects. ~ Matthew Gates, Alex Potanin. https://arxiv.org/abs/2502.11344 #ITP #Coq #Rocq
arXiv.orgA Coq implementation of a Theory of Tagged ObjectsWe present a first step towards the Coq implementation of the Theory of Tagged Objects formalism. The concept of tagged types is encoded, and the soundness proofs are discussed with some future work suggestions.