Stream: Miscellaneous

Topics:

• Proof theory Q - cut elimination (9 messages, latest: Mar 21 2023 at 14:41)
• Project Euler Problem 3 (2 messages, latest: Mar 14 2023 at 23:38)
• Proof Planning (3 messages, latest: Mar 14 2023 at 06:51)
• Zulip archive (59 messages, latest: Mar 12 2023 at 21:42)
• Machine Assisted Proofs videos are now available (1 message, latest: Mar 11 2023 at 16:22)
• Support Zulip (1 message, latest: Mar 09 2023 at 15:36)
• Easycrypt (7 messages, latest: Mar 07 2023 at 17:35)
• Category theory foundations? (37 messages, latest: Mar 04 2023 at 14:21)
• Mizar (2 messages, latest: Mar 02 2023 at 19:55)
• Finite Fields automation ? (1 message, latest: Mar 02 2023 at 16:49)
• New stack exchange for PL (9 messages, latest: Mar 02 2023 at 13:43)
• Coq in the wild (12 messages, latest: Feb 27 2023 at 17:15)
• Sorting subarrays (21 messages, latest: Feb 23 2023 at 07:38)
• New Discourse topics (42 messages, latest: Feb 15 2023 at 20:49)
• what is strong lemma and what is weaker lemma (2 messages, latest: Feb 14 2023 at 08:55)
• GPTChat (66 messages, latest: Feb 13 2023 at 14:40)
• Coherence Spaces (5 messages, latest: Feb 11 2023 at 10:04)
• ✔ Other possible names for Coq (4 messages, latest: Feb 10 2023 at 17:46)
• ✔ Whitelist of proof starters and enders (11 messages, latest: Feb 09 2023 at 08:57)
• Coq and Cyber Resilience Act (17 messages, latest: Feb 07 2023 at 12:28)
• ✔ can Semantic Typing be done in coq? (6 messages, latest: Feb 01 2023 at 16:17)
• Content about System F (Polymorphic Lambda Calculus)) (11 messages, latest: Feb 01 2023 at 02:57)
• Structure preserving translation (27 messages, latest: Jan 31 2023 at 13:44)
• Improve intuition and speed (10 messages, latest: Jan 30 2023 at 10:53)
• Universities teaching Coq (18 messages, latest: Jan 16 2023 at 10:24)
• terminating type checker with untyped conversion and fuel (107 messages, latest: Jan 15 2023 at 21:57)
• Project File Problem (1 message, latest: Jan 08 2023 at 08:39)
• Games and puzzles (4 messages, latest: Jan 04 2023 at 20:57)
• Grad School (Sorry that I am being bit off topic) (5 messages, latest: Jan 02 2023 at 23:37)
• Chúc mừng năm mới (1 message, latest: Dec 31 2022 at 10:40)
• 7 pages, 4 colors, allegedly (5 messages, latest: Dec 22 2022 at 05:09)
• ✔ Work in Scratch but not in File (8 messages, latest: Dec 20 2022 at 00:23)
• Do mathematicians really care about truth? (19 messages, latest: Dec 17 2022 at 19:38)
• Conservativity of CC_obs' over ZFC (3 messages, latest: Dec 16 2022 at 22:39)
• Why is UIP not a lemma (47 messages, latest: Dec 15 2022 at 23:54)
• - (6 messages, latest: Dec 15 2022 at 12:15)
• Anyone from Latvia? (3 messages, latest: Dec 14 2022 at 18:48)
• IETF formal methods (14 messages, latest: Dec 13 2022 at 19:51)
• Not being able to write pen and paper proofs (20 messages, latest: Dec 08 2022 at 20:27)
• Extraction of interaction trees (6 messages, latest: Dec 07 2022 at 16:59)
• adventofcode.com/2022 (8 messages, latest: Dec 06 2022 at 19:58)
• Automatic formalization (15 messages, latest: Nov 25 2022 at 10:50)
• Javascript and verified programs? (8 messages, latest: Nov 22 2022 at 16:01)
• Why int instead of bool bad? (8 messages, latest: Nov 18 2022 at 15:58)
• IRC integration for Zulip (6 messages, latest: Nov 18 2022 at 14:36)
• What would be a theory for dealing with n-bits arithmetics ? (18 messages, latest: Nov 18 2022 at 08:55)
• Combining CECILL-2.1, LGPL, and CECILL-B/C (24 messages, latest: Nov 09 2022 at 18:32)
• job announcements (8 messages, latest: Nov 02 2022 at 17:02)
• Is it possible to do computerized proof as work? (12 messages, latest: Oct 29 2022 at 02:48)
• Hashmap formalization (34 messages, latest: Oct 21 2022 at 16:43)
• ✔ chomp10s proof help (10 messages, latest: Oct 16 2022 at 19:37)
• Methodology for coming up with lemmas (13 messages, latest: Oct 14 2022 at 22:16)
• logic quiz (5 messages, latest: Oct 10 2022 at 08:27)
• Standard ML vs (O)Caml (69 messages, latest: Oct 08 2022 at 20:46)
• Progress and preservation proofs for dependent types (84 messages, latest: Oct 06 2022 at 05:00)
• CC0 for software (34 messages, latest: Sep 28 2022 at 16:26)
• Bonn: two professorships in formal maths (1 message, latest: Sep 23 2022 at 17:57)
• Encoding indexes with equalities (16 messages, latest: Sep 19 2022 at 11:56)
• Memes (3 messages, latest: Sep 14 2022 at 16:10)
• Formal proof failures (53 messages, latest: Sep 07 2022 at 20:42)
• Survey results feedback (1 message, latest: Aug 31 2022 at 16:04)
• ✔ Coq docs working? (5 messages, latest: Aug 30 2022 at 11:43)
• Serious research forum (7 messages, latest: Aug 27 2022 at 19:11)
• GitHub markdown supports LaTeX math expressions (1 message, latest: Aug 24 2022 at 21:02)
• Old Coq modules (34 messages, latest: Aug 18 2022 at 12:15)
• Plugin development with Coq-Elpi, Template/MetaCoq, Mtac2... (72 messages, latest: Aug 16 2022 at 15:20)
• Logo for the Coq Zulip (1 message, latest: Aug 11 2022 at 22:24)
• BIRS workshop on formalization of cohomology theories (1 message, latest: Aug 11 2022 at 14:51)
• Homebrew issues (2 messages, latest: Aug 11 2022 at 14:03)
• Collacoq (50 messages, latest: Aug 05 2022 at 09:24)
• EuroProofNet Workshop on libraries of formal proofs (3 messages, latest: Aug 04 2022 at 19:22)
• FLOC 2022 (4 messages, latest: Aug 04 2022 at 19:05)
• Any other interesting ideas (what to offer in patreon.com) (20 messages, latest: Aug 03 2022 at 07:23)
• hal.inria.fr inactive? (6 messages, latest: Jul 28 2022 at 16:05)
• New plugin to work with commutative diagrams (11 messages, latest: Jul 21 2022 at 10:53)
• Kevin Buzzard interview about Lean (124 messages, latest: Jul 11 2022 at 13:33)
• Formalization of low level information flow (1 message, latest: Jul 01 2022 at 20:40)
• An infinite sum (8 messages, latest: Jun 30 2022 at 03:06)
• ✔ User Abusing the System for Homework Problem? (4 messages, latest: Jun 22 2022 at 00:25)
• Docker images based on oldstable (1 message, latest: Jun 14 2022 at 19:19)
• PR notification spam (5 messages, latest: Jun 07 2022 at 20:31)
• ✔ Docker image with Alectryon (11 messages, latest: May 31 2022 at 09:37)
• ✔ Understanding a proof (16 messages, latest: May 16 2022 at 06:17)
• Is classical logic wrong? (46 messages, latest: May 15 2022 at 15:06)
• types 2022 (1 message, latest: May 04 2022 at 14:34)
• Coq and statistics - any suggestions for bachelor thesis? (17 messages, latest: May 01 2022 at 19:26)
• Properties of logic (14 messages, latest: Apr 30 2022 at 16:23)
• stream events (2 messages, latest: Apr 14 2022 at 09:34)
• Resources to get started with Coq (6 messages, latest: Apr 09 2022 at 11:33)
• miniF2F (1 message, latest: Mar 24 2022 at 15:41)
• Difference: Proof vs model checking (64 messages, latest: Mar 22 2022 at 20:28)
• ctags for Coq (4 messages, latest: Mar 20 2022 at 16:24)
• web public streams (24 messages, latest: Mar 16 2022 at 15:56)
• newman's lemma and hidley rose lemma (12 messages, latest: Mar 07 2022 at 08:06)
• Formal verification in industry (9 messages, latest: Feb 28 2022 at 18:08)
• Workshop posted on discourse (5 messages, latest: Feb 28 2022 at 16:19)
• Help finding papers for NOL talk (10 messages, latest: Feb 22 2022 at 17:58)
• Scientific and technical open source software award to Coq (3 messages, latest: Feb 05 2022 at 18:15)
• Shallow vs deep embedding (65 messages, latest: Feb 04 2022 at 12:34)
• Green's theorem? (2 messages, latest: Feb 01 2022 at 09:09)
• deleting pages doesn't appear in zulip notifications (8 messages, latest: Jan 26 2022 at 13:09)
• Linter for unused hypotheses (2 messages, latest: Jan 25 2022 at 20:32)
• formal specification of Common Lisp in Coq (3 messages, latest: Dec 25 2021 at 22:16)
• Formal methods course list (3 messages, latest: Dec 23 2021 at 15:12)
• Papers that reference Coq code inline (6 messages, latest: Dec 14 2021 at 22:06)
• Proof Assistant StackExchange Proposal (66 messages, latest: Dec 09 2021 at 13:25)
• QuickChick installation issues (1 message, latest: Dec 09 2021 at 09:41)
• Lifting Prop to Type without inductive types (8 messages, latest: Dec 08 2021 at 16:10)
• Thesis defense for Clément Pit-Claudel (9 messages, latest: Dec 08 2021 at 08:48)
• Citation for propositional vs setoid equality (71 messages, latest: Dec 07 2021 at 23:57)
• Computer Algebra Systems for pedagogical purposes? (5 messages, latest: Dec 02 2021 at 04:08)
• Symbols for Leibniz, definitional, and syntactic equalities (22 messages, latest: Nov 29 2021 at 06:40)
• Elementary questions on Zulip and Stack Exchange (17 messages, latest: Nov 25 2021 at 17:14)
• JFP goes author pays (25 messages, latest: Nov 22 2021 at 16:00)
• dependent sum types in HoTT (8 messages, latest: Nov 08 2021 at 20:48)
• Attacks by using Unicode to inject invisible source code (3 messages, latest: Nov 04 2021 at 12:34)
• First person pronoun in English papers (18 messages, latest: Nov 03 2021 at 07:39)
• Default subscribed streams (12 messages, latest: Oct 24 2021 at 20:39)
• Advice on publishing Coq developments (16 messages, latest: Oct 06 2021 at 18:43)
• 20M USD for Lean and Mathlib (3 messages, latest: Oct 06 2021 at 15:15)
• 4CT and type checkers (36 messages, latest: Oct 03 2021 at 23:26)
• Github email notification settings (10 messages, latest: Sep 26 2021 at 14:46)
• Redmonk July 2021 report (10 messages, latest: Sep 19 2021 at 10:10)
• ✔ Initial objects in Coq? (7 messages, latest: Sep 18 2021 at 04:19)
• Coq and Lean on StackOverflow (29 messages, latest: Sep 14 2021 at 16:31)
• JAR paper on export of the Coq opam archive (3 messages, latest: Sep 12 2021 at 08:03)
• category-theory library in Coq's CI (24 messages, latest: Sep 03 2021 at 08:16)
• opam switch tight to a directory? (3 messages, latest: Aug 29 2021 at 03:39)
• Ph.D. on formalizing complexity classes (39 messages, latest: Aug 20 2021 at 11:26)
• Formalizing undergraduate type theory (14 messages, latest: Aug 14 2021 at 22:20)
• link detection (5 messages, latest: Aug 09 2021 at 11:39)
• alt-ergo (40 messages, latest: Aug 06 2021 at 13:43)
• Github citations (1 message, latest: Jul 30 2021 at 08:51)
• Official name of Coq (260 messages, latest: Jul 22 2021 at 12:42)
• Remove dead code (3 messages, latest: Jul 12 2021 at 11:03)
• Coq course for beginner mathematics? (12 messages, latest: Jul 06 2021 at 11:14)
• Github copilot (3 messages, latest: Jun 30 2021 at 08:33)
• Coq club archives (4 messages, latest: Jun 16 2021 at 08:55)
• default language (2 messages, latest: Jun 11 2021 at 15:02)
• non standard integers (14 messages, latest: Jun 04 2021 at 01:09)
• induction exercise hint (8 messages, latest: May 18 2021 at 10:10)
• Does Coq follow a context-free grammar? (16 messages, latest: Apr 27 2021 at 09:38)
• How things could have been phrased better in the logo + n... (40 messages, latest: Apr 17 2021 at 15:28)
• Measuring proof assistant ecosystems (66 messages, latest: Apr 14 2021 at 07:40)
• Online Coq talks (15 messages, latest: Apr 13 2021 at 09:42)
• Certified Elm web-apps (17 messages, latest: Apr 12 2021 at 13:52)
• Official name of Coq's type theory (59 messages, latest: Apr 12 2021 at 08:18)
• coq api documentation on github (2 messages, latest: Apr 05 2021 at 15:30)
• Proof Ground 2021 (2 messages, latest: Mar 29 2021 at 09:36)
• Extraction of Zarith (9 messages, latest: Mar 28 2021 at 17:19)
• Finmap construction (1 message, latest: Mar 25 2021 at 12:58)
• native compute (17 messages, latest: Mar 25 2021 at 11:07)
• verifying a compiler without CompCert (3 messages, latest: Mar 15 2021 at 15:42)
• Multithreaded coq/proofgeneral? (9 messages, latest: Mar 14 2021 at 19:55)
• Advice for a new Zulip chat? (24 messages, latest: Mar 03 2021 at 16:17)
• Nix for Lean and for Coq (99 messages, latest: Feb 28 2021 at 10:46)
• Extraction examples (3 messages, latest: Feb 10 2021 at 04:07)
• mechanized/formalized (11 messages, latest: Feb 08 2021 at 14:36)
• Zulip preview feature (20 messages, latest: Jan 27 2021 at 20:18)
• Streaming proof assistant use (31 messages, latest: Jan 15 2021 at 23:30)
• Vernacstate.Declare.get_current_proof_name (1 message, latest: Jan 11 2021 at 20:46)
• Snap package (26 messages, latest: Jan 05 2021 at 19:16)
• Lean Together 2021 (21 messages, latest: Jan 05 2021 at 10:06)
• Math/CS 2020 breakthroughs (4 messages, latest: Jan 03 2021 at 15:51)
• How to troubleshoot coqbot? (1 message, latest: Dec 12 2020 at 16:59)
• Formal theories and Provability Logic in Coq (32 messages, latest: Dec 02 2020 at 08:24)
• native compute on mac (9 messages, latest: Nov 24 2020 at 08:09)
• Coq illustrations (3 messages, latest: Nov 21 2020 at 22:25)
• Quick reference (2 messages, latest: Nov 16 2020 at 23:02)
• OCaml User Survey (63 messages, latest: Nov 16 2020 at 18:27)
• Anyone applying for faculty positions this year? (4 messages, latest: Nov 15 2020 at 18:08)
• Autosubst1 and Autosubst2 (45 messages, latest: Nov 12 2020 at 14:22)
• Proof General really slow? (33 messages, latest: Nov 03 2020 at 15:42)
• Using Coq in GNAT Studio (10 messages, latest: Nov 03 2020 at 14:10)
• General constructive math stream? (15 messages, latest: Oct 27 2020 at 14:13)
• Show (4 messages, latest: Oct 26 2020 at 17:02)
• Tinkering with (very) basic model theory (1 message, latest: Oct 23 2020 at 16:50)
• Is it okay to ask mathy questions here? (2 messages, latest: Oct 22 2020 at 17:34)
• Quanta Magazine article on formalized math libraries (99 messages, latest: Oct 16 2020 at 08:11)
• Learning category theory as a programmer (63 messages, latest: Oct 11 2020 at 10:52)
• A practical use of quickchick (1 message, latest: Oct 07 2020 at 14:18)
• Native arrays (36 messages, latest: Oct 01 2020 at 23:27)
• CC EAL7 (15 messages, latest: Oct 01 2020 at 13:27)
• To SSReflect or to not SSReflect? (1 message, latest: Oct 01 2020 at 07:11)
• Discourse and Zulip announcements (9 messages, latest: Oct 01 2020 at 03:26)
• Collect pairs of goals and tactics (3 messages, latest: Sep 25 2020 at 13:46)
• Automatically hide proof witnesses? (43 messages, latest: Sep 25 2020 at 00:25)
• coq.io (4 messages, latest: Sep 24 2020 at 09:45)
• Cauchy real in coq-hott (3 messages, latest: Sep 16 2020 at 12:42)
• Formalizing undergraduate mathematics (58 messages, latest: Sep 11 2020 at 17:59)
• Strict positivity requirement (13 messages, latest: Sep 11 2020 at 13:54)
• load_vernac (4 messages, latest: Sep 10 2020 at 15:58)
• Extraction to Ocaml ints (7 messages, latest: Sep 09 2020 at 11:52)
• jscoq and SF (29 messages, latest: Sep 07 2020 at 11:27)
• Github for education (13 messages, latest: Sep 06 2020 at 15:04)
• Github problems (4 messages, latest: Sep 04 2020 at 11:04)
• Transferring Coqtail/Coq100 to coq-community (26 messages, latest: Sep 01 2020 at 15:44)
• Disappearing papers and disappearing proofs (7 messages, latest: Aug 31 2020 at 10:55)
• Industrial uses of ITP (2 messages, latest: Aug 30 2020 at 11:19)
• Umbrella library for Coq (70 messages, latest: Aug 29 2020 at 14:47)
• remove duplicate account (16 messages, latest: Aug 29 2020 at 10:16)
• Etiquette on cross-posting between discourse and Coq-club (40 messages, latest: Aug 18 2020 at 17:01)
• Evidence of superiority of Concurrent Separation Logic (20 messages, latest: Aug 18 2020 at 06:39)
• Problems with accessing old Marelle web (7 messages, latest: Aug 17 2020 at 08:22)
• Zulip stream on AI and hammers? (8 messages, latest: Aug 09 2020 at 06:16)
• Gpgpu application of coq (3 messages, latest: Aug 06 2020 at 20:26)
• MLCompcert (2 messages, latest: Aug 06 2020 at 09:18)
• "formal verification" (30 messages, latest: Aug 02 2020 at 14:07)
• Information on CompCert (2 messages, latest: Jul 31 2020 at 14:28)
• Readings on equality relation (22 messages, latest: Jul 24 2020 at 22:49)
• Relocating and renaming topics (37 messages, latest: Jul 16 2020 at 00:04)
• fancy exception modules (3 messages, latest: Jul 13 2020 at 14:22)
• Verified textbook algorithms (13 messages, latest: Jul 11 2020 at 17:32)
• TCB snobbery (51 messages, latest: Jul 09 2020 at 16:57)
• Zulip is killing Discourse? (46 messages, latest: Jul 05 2020 at 12:19)
• Proof ground (56 messages, latest: Jul 04 2020 at 07:24)
• Coq session at IJCAR 2020 (13 messages, latest: Jul 03 2020 at 13:10)
• Chances for Coq on new ARM Macs? (6 messages, latest: Jul 01 2020 at 14:42)
• Size of proof repositories (15 messages, latest: Jun 30 2020 at 13:55)
• Zulip dump (2 messages, latest: Jun 24 2020 at 21:38)
• Permissions (12 messages, latest: Jun 24 2020 at 13:43)
• Type theories vs. propositions-as-types (21 messages, latest: Jun 22 2020 at 20:56)
• Lean 4 release end of summer (4 messages, latest: Jun 21 2020 at 12:44)
• Discussing the new Discourse integration (11 messages, latest: Jun 19 2020 at 09:38)
• Discussing Lean's foundations (92 messages, latest: Jun 13 2020 at 20:19)
• Lean vs. Coq release management (31 messages, latest: Jun 07 2020 at 22:47)
• Mathematicians learning to use proof assistants (1 message, latest: Jun 07 2020 at 22:46)
• Gitter Features on Zulip (3 messages, latest: Jun 06 2020 at 16:52)
• SerAPI vs. SErAPIS (1 message, latest: Jun 05 2020 at 22:52)
• Zulip CPU Usage (3 messages, latest: May 31 2020 at 23:48)
• Yay Zulip (1 message, latest: May 22 2020 at 07:31)
• Stream creation and naming policy (42 messages, latest: May 20 2020 at 09:30)
• Experimental Mathematics Special Issue on ITP in Mathematics (17 messages, latest: May 19 2020 at 16:46)
• Coq Zulip archive (3 messages, latest: May 16 2020 at 14:14)
• Going out (8 messages, latest: May 12 2020 at 19:18)
• New users (2 messages, latest: May 11 2020 at 08:55)
• Bench notifications (5 messages, latest: May 10 2020 at 10:36)

Last updated: Mar 25 2023 at 07:28 UTC