#coq — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #coq, aggregated by home.social.
-
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
-
@jastrow @helenecollon @Khrys Oui à priori (photo bof). Les corneilles d'ici, d'Amérique, sont souvent confondues avec les grands corbeaux. C'est leur cri, la forme de leur bec mais surtout en vol qu'on les distingue le mieux car l'apparence de la queue fait la différence et enlève les doute (moi c'est comme ça que je suis certaine). J'ai retenu que la corneILLe à un éventaILLE 😉 PVI: https://mffp.gouv.qc.ca/jeunesse/grand-corbeau-corneille-amerique/ #amatrice #ornithologie #COQ https://www.coq.qc.ca/fr/accueil
-
C'est moi qui vous réveille avec le chant du #coq ce matin ! 🙂
Je ne pense pas rien stooler en publiant ce post ce matin. C'était la commande que j'ai reçu pour un collectionneur de coqs ! Il l'a en principe reçu hier en cadeau de son épouse! J'espère qu'il l'aime! Parfois j'ai de leur nouvelles.
100% rebut
Bonne journée à toutes et tous!
#art #sculpture #scrapmetalart #metal_artetalArt #recycling #rooster #acier #steel
-
Coq: The World's Best Macro Assembler? [pdf] [2013]
https://nickbenton.name/coqasm.pdf
#HackerNews #Coq #Macro #Assembler #HackerNews #PDF #2013 #Programming
-
@grogpod I loved both of your episodes on caves of qud. Was kind of nervous about your reactions to it but it turned out great... Btw was Will not there because he didn't like it and you were afraid of your reputation score going down? Lol
-
More Qud sprites! I made these to help out in a mod jam this halloween c: I'll share the mod when it's up on the steam workshop!
#cavesofqud #fanart #coq #pixelart #alien #illithid #xenomorph
-
CW: AI and a11y (+)
A few years ago, I learned how to use #Coq, a proof assistant, by reading a wonderful freely available book called software Foundations (I think it was called something else at the time). This resource was, as well as an excellent introduction for a user who hadn't done (almost) any proof assistant stuff before, accessible for a blind person. It was easy to read the .v files and follow along filling in the exercises.
A bit later, Coq changed its interface. Specifically, coqtop, which is the command-line REPL-ish way to use coq, removed the capability to show proof scripts (Show Script) and the automatic script printing after Qed/Defined/Admitted/etc. This made it very hard for me to keep using it, because the IDEs were not accessible at the time (nor now).
Recently I used #Codex, specifically codex-cli, to solve this problem. I asked it to write me a script that would sit between me and coqtop, and allow me to enter theorems, tactics, etc, and keep a record of them on a .v file, including tactics only when they succeeded, and unwinding when the undo command was used. Codex took a while flailing, and I had to direct its attempts carefully, but it got a script that works, written in python, to do just this. I can now use Coq again, and I get usable .v files afterwards which I can work on.
In principle this is something I could have done myself. But the python script is fairly large, and the task is fiddly (requires messing about detecting prompts, etc). Realistically, I think I would never have done it. My next possibility was trying to use Coq from VS Code, but I don't know how well that would have worked out.
So, in this particular case, an AI coding agent made #accessibility where there was none and increased my ability to learn and work. It's going to be difficult to convince me that this has no value.
Yes, I asked the Coq-Club mailing list for solutions to this problem. None were offered.
Also if anyone needs this script let me know.
-
#year1783 (1/2) :
- USA : fin guerre civile pour l'Indépendance (cf 1775 1776 1777).“La guerre fut aussi une lutte entre colons et Amérindiens, entre esclavagistes et esclaves.”
- Royaume catholique France Navarre Ancien Régime -> Château Versailles (cf 1...) avec le Roi Louis 16 -> expériences aéronautiques #hydrogene avec Étienne de Montgolfier vol avec 1 #canard 1 #coq 1 #mouton dans panier osier attaché à ballon à #air chaud (cf 19..) ...
-
Caves of Qud Wins Hugo Award for Best Game or Interactive Work
https://fullcleared.com/news/caves-of-qud-wins-hugo-award-for-best-game-or-interactive-work/
#gaming #gamingnews #videogames #hugoawards #coq #cavesofqud
-
Readings shared July 14, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/15-readings_shared_07-14-25 #Coq #ITP #IsabelleHOL #LLMs #LeanProver #Math
-
Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. https://arxiv.org/abs/2507.06360v1 #ITP #Coq
-
Les trois bizarres de la #basseCour, ceux qui sont toujours derrière toi quand tous les autres sont partis.
Il y a Jean-Gab, le #canard moche mais sympas. Souvent il s'avance vers toi en ayant l'air de se tripoter les mains dans le dos, timide mais cou tendu : "bouffe ? oh, sans vouloir vous déranger, hein".
Et puis deux "broilers brothers", comme des chats, ils vont où on est et ils se couchent pas loin… ou devrais-je dire ils s’assoient… ou… mais sérieux, c'est quoi cette position ?
#coq -
Readings shared April 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/13-readings_shared_04-13-25 #AI #ATP #Coq #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Mace4 #Math #Prover9 #SetTheory
-
A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=10930874 #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
-
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
-
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
-
Oh hey, Asterisk has an article on theorem provers, LLMs, and autoformalization (i.e. automatically turning math papers into formalized proofs). I still think this task is significantly more difficult than what some people seem to think, but who can really tell anymore at this point.
asteriskmag.com/issues/09/automating-math
#TheoremProvers #Coq #Lean #Isabelle -
Laws of quantum programming. ~ Mingsheng Ying, Li Zhou, Gilles Barthe. https://arxiv.org/abs/2412.19463 #ITP #Coq #Rocq #QuantumProgramming
-
Readings shared December 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/13-readings_shared_12-13-24 #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math
-
Learning rules explaining interactive theorem proving tactic prediction. ~ Liao Zhang, David M. Cerna, Cezary Kaliszyk. https://arxiv.org/abs/2411.01188 #ILP #ITP #Coq
-
Readings shared September 28, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/28-readings_shared_09-28-24 #ITP #LeanProver #IsabelleHOL #Coq #HOL_Light #Logic #Math
-
Readings shared September 2, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/02-readings_shared_09-02-24 #ITP #Lean4 #LeanProver #IsabelleHOL #Coq #Maude #Math #Calculemus #FunctionalProgramming
-
Readings shared August 20, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/21-readings_shared_08-20-24 #ITP #Lean4 #Coq #ACL2 #AlphaProof #Math #Haskell #FunctionalProgramming #Logic #Math #CategoryTheory #TypeTheory
-
Lecturas compartidas el 26 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/27-lecturas_compartidas_el_26-jul-24 #ITP #Lean4 #IsabelleHOL #Coq #Math #IMO #AI #AlphaProof #FunctionalProgramming #Haskell
-
Lecturas compartidas el 25 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/26-lecturas_compartidas_el_25-jun-24 #ITP #Agda #Coq #HOL #HOL_Light #IsabelleHOL #Lean4 #Metamath #Math #Haskell #Python #Algorithms #AI #MachineLearning
-
My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!
Who? anyone who uses or has used an interactive theorem prover for whatever purpose
What? 90 - 120 minute interviews (possibly including a small think-aloud programming session)
When? interviews will be scheduled starting September 2024
Where? online (participants from anywhere are welcome)
We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.
Sign up here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy
-
#coq #dependent-types #typetheory Handling impossible match arms in Coq (https://www.unwoundstack.com/blog/dependent-matching-in-coq.html)
-
Lecturas compartidas el 30 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/05/31-lecturas_compartidas_el_30-may-24 #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs
-
Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. https://easychair.org/publications/paper/mtFT #ITP #HOL_Light #Coq
-
Lecturas compartidas el 11 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-11-de-mayo #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
-
Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. https://arxiv.org/abs/2405.04699 #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math
-
Lecturas compartidas el 8 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-8-de-mayo #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math
-
Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. https://files.inria.fr/blanqui/lpar24.pdf #ITP #HOL_Light #Coq
-
Lecturas compartidas el 18 de abril de 2024. https://jalonso.substack.com/lecturas-compartidas-el-18-de-abril #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Imandra #ATP #SMT #AI #DeepLearning #Math #CategoryTheory
-
Lecturas compartidas el 16 de marzo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-16-de-marzo #Coq #FormalVerification #ILP #ITP #IsabelleHOL #Lean4 #LogicProgramming #SMT #cvc5
-
Playing #CavesOfQud and damn is it frustrating trying to get into another roguelike and not understanding all the keybindings like I do in #CDDA but I'm having a lot of fun.
...I also had a very very short run earlier where I tried to talk to the starting quest giver and accidentally threw an EMP grenade at his head... My ignorence was promptly ventilated.
-
"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
- Jacob Lurie