#CallForPresentations #CoqPL #CoqPL2024 (Workshop on Coq for Programming Languages) "provide[s] an opportunity for programming languages researchers and practitioners with an interest in Coq to meet and interact with one another and members from the core Coq development team... To foster open discussion of cutting edge research which can later be published in full conference proceedings, we will not publish papers from the workshop" https://popl24.sigplan.org/home/CoqPL-2024#Call-for-Presentations #Coq #ITP #PL #POPL

Verified compilation (An introduction to CompCert). ~ Sandrine Blazy. https://people.irisa.fr/Sandrine.Blazy/2023-VTSA/2023vtsa.pdf #ITP #Coq

This is probably really easy but is the variant of LEM (forall a, not a or not not a) equivalent to vanilla LEM (for all a, a or not a) constructively?
Bonus points if you can give me a runnable example
#logic #agda #coq #idris

Formalizing hyperspaces for extracting efficient exact real computation. ~ Michal Konečný, Sewon Park, Holger Thies. https://drops.dagstuhl.de/opus/volltexte/2023/18593/pdf/LIPIcs-MFCS-2023-59.pdf #ITP #Coq

A formalized extension of the substitution lemma in Coq. ~ Maria J. D. Lima, Flávio L. C. de Moura. https://flaviomoura.info/files/from2023.pdf #ITP #Coq

Interaction trees and formal specifications. ~ Lucas Silver. https://www.seas.upenn.edu/~lucsil/assets/pdf/dissertation.pdf #ITP #Coq

Automating the formal verification of software. ~ Emily First. https://scholarworks.umass.edu/cgi/viewcontent.cgi?article=3936&context=dissertations_2 #ITP #Coq

Formalizing the unexpected hanging paradox: A classical surprise. ~ Polina Vinogradova. https://link.springer.com/chapter/10.1007/978-3-031-40875-5_4 #ITP #Coq

Formalizing monoidal categories and actions for syntax with binders. ~ Benedikt Ahrens, Ralph Matthes, Kobe Wullaert. https://arxiv.org/abs/2307.16270 #ITP #Coq

@Ajo1322 Caves of Qud.
I bought it two weeks ago and it will get a proper release next year.
#CoQ #cavesofqud

Formalizing the query language of Semantic MediaWiki. ~ Marijn van Wezel. https://www.cs.ru.nl/bachelors-theses/2023/Marijn_van_Wezel___1040392___Formalizing_the_query_language_of_Semantic_MediaWiki.pdf #ITP #Coq

Testing equality of parametric semi-linear sets. ~ Engel Lefaucheux. https://inria.hal.science/hal-04172593/document #ITP #Coq #Math

Learning proof transformations and its applications in interactive theorem proving. ~ Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban. http://cl-informatik.uibk.ac.at/users/cek/docs/23/lzlbckju-frocos23.pdf #ITP #Coq #MachineLearning

Books series on formal verification of the programs, logic programming, theorem provers and coq.

https://softwarefoundations.cis.upenn.edu/

#book #books #coq #logic #verification

A Cheat Sheet for #Coq Proof Assistant users who are interested in #LeanProver

The repo includes an A4 pdf that you can print out and put on your wall for easy reference

https://github.com/katydid/coq-lean-cheatsheet/

@bon @screwtape

Synthetic undecidability and incompleteness of first‑order axiom systems in Coq. ~ Dominik Kirst, Marc Hermes. https://publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/35767/1/s10817-022-09647-x.pdf #ITP #Coq #Logic

Bibliothèque certifiée en Coq pour la provenance des données. ~ Rébecca Zucchini. https://www.theses.fr/2023UPASG040.pdf #ITP #Coq

LeanProver - A Cheat Sheet for those familiar with Coq Proof Assistant. ~ Walter Schulze (@awalterschulze ). https://youtu.be/zjEkr-zBf1Q #ITP #Lean4 #Coq

A sound and complete projection for global types. ~ Dawit Tirore, Jesper Bengtson, Marco Carbone. https://drops.dagstuhl.de/opus/volltexte/2023/18374/pdf/lipics-vol268-itp2023-complete.pdf#page=489 #ITP #Coq

Proof repair infrastructure for supervised models: Building a large proof repair dataset. ~ Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer. https://drops.dagstuhl.de/opus/volltexte/2023/18374/pdf/lipics-vol268-itp2023-complete.pdf#page=451 #ITP #Coq