Readings shared May 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/04-readings_shared_05-04-25 #ACL2 #Coq #FunctionalProgramming #Haskell #ITP #Math #Rocq

Formalizing reversible computations for synchronous dataflow languages with infinite lists. ~ Sosuke Moriguchi et als. https://www.atlantis-press.com/article/126010278.pdf #ITP #Coq #Rocq

Formalizing resource ownership semantics of spinlocks with the Coq proof assistant. ~ Sebastian Luis S. Ortiz et als. https://www.atlantis-press.com/article/126010274.pdf #ITP #Coq #Rocq

Readings shared May 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/02-readings_shared_05-02-25 #AI #ChatGPT #DeepSeek #ITP #IsabelleHOL #LLMs #LeanProver #Math #Python #Rocq

Semantics of probabilistic programs using s-finite kernels in dependent type theory. ~ Reynald Affeldt, Cyril Cohen, Ayumu Saito. https://dl.acm.org/doi/pdf/10.1145/3732291 #ITP #Rocq

Readings shared April 30, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/30-readings_shared_04-30-25 #ITP #Coq #Rocq #LeanProver

Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. https://infoscience.epfl.ch/server/api/core/bitstreams/c88d5882-a045-476a-935d-7e3216e2d097/content #ITP #Coq #Rocq

https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001

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

Readings shared April 11, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/11-readings_shared_04-11-25 #Agda #Coq #FunctionalProgramming #Hakell #Haskell #ITP #IsabelleHOL #LeanProver #Math #Rocq #SetTheory

A comparative review of ZFC, NBG, and MK axiom systems: Theoretical foundations and formalization in Coq. ~ Si Chen, Wensheng Yu. https://www.preprints.org/manuscript/202504.0684/v1 #ITP #Coq #Rocq #Math #SetTheory

Code generation via meta-programming in dependently typed proof assistants. ~ Mathis Bouverot-Dupuis, Yannick Forster. https://hal.science/hal-05024207/document #ITP #Agda #Rocq #LeanProver

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. https://discourse.rocq-prover.org/t/looking-for-testers-for-proofgeneral-coq9-rocq-cli/2590
and https://github.com/ProofGeneral/PG/issues

#rocq #rocq_prover #ProofGeneral

Readings shared March 27, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/27-readings_shared_03-27-25 #CLP #Coq #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #LogicProgramming #Math #ProgramaciónFuncional #Prolog #Rocq #TeXLaTeX

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

PHOASでshift/resetのCPS変換 in Rocq(旧Coq)
https://qiita.com/mrkbc/items/89b034dadc69df2ad274?utm_campaign=popular_items&utm_medium=feed&utm_source=popular_items

#qiita #Coq #限定継続 #rocq

Apparently, the #Rocq Prover version 9.0 is out. The end of an era. Good job to everyone involved! #Coq

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.

#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey

Readings shared March 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/10-readings_shared_03-10-25 #CommonLisp #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #LogicProgramming #Lógica #Matemática #Math #Prolog #Rocq

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