Zulip Chat Archive

Stream: Program verification

Topics:

Monadic program logic: Request for feedback (31 messages, latest: May 01 2025 at 18:28)
Collecting small program verification examples (6 messages, latest: Apr 30 2025 at 13:48)
Request for Feedback: Lean 4 Proof related to P=NP (80 messages, latest: Apr 29 2025 at 16:12)
Complexity Theory Definitions and Axioms (3 messages, latest: Apr 29 2025 at 09:03)
Legal and Lean (6 messages, latest: Apr 16 2025 at 11:55)
Montgomery and signed Barrett reduction (5 messages, latest: Apr 02 2025 at 09:08)
Tamarin (<->? Lean) / Security Protocol Verification (25 messages, latest: Mar 26 2025 at 12:23)
Projects (78 messages, latest: Mar 03 2025 at 03:08)
Algorithms in Lean (37 messages, latest: Mar 03 2025 at 01:56)
How to reason formally about optimisation in games? (3 messages, latest: Feb 15 2025 at 06:51)
How to reason about operations on fixed size integers ? (8 messages, latest: Jan 31 2025 at 14:52)
Cases on operational semantics relation (1 message, latest: Jan 23 2025 at 16:29)
Is anyone else working on Iris in Lean? (9 messages, latest: Jan 22 2025 at 09:46)
Friendly challenge :).html) (28 messages, latest: Jan 05 2025 at 20:50)
Concurrent and distributed programs (4 messages, latest: Dec 30 2024 at 11:50)
✔ Decomposing UInt32 (22 messages, latest: Dec 11 2024 at 20:42)
Problem with USize (9 messages, latest: Nov 26 2024 at 20:48)
Model Checking (26 messages, latest: Nov 25 2024 at 12:12)
✔ Stuck on proving correctness of a DP algorithm (5 messages, latest: Nov 07 2024 at 22:52)
Termination for Rewrite Validity Proof (1 message, latest: Oct 22 2024 at 21:18)
✔ Termination and Trees (6 messages, latest: Oct 21 2024 at 15:28)
Intrinsic or Extrinsic Typing for PL Metatheory? (10 messages, latest: Oct 11 2024 at 02:29)
Decidability of List.Mem (24 messages, latest: Oct 06 2024 at 07:04)
[x,y] vs x::y::nil (8 messages, latest: Oct 05 2024 at 17:17)
ofBool in bv_decide? (9 messages, latest: Oct 05 2024 at 15:08)
iterator over list is an element of the list (lean4) (6 messages, latest: Sep 28 2024 at 03:05)
Recursion with HList (10 messages, latest: Sep 05 2024 at 14:24)
theorem on ranges (8 messages, latest: Aug 27 2024 at 23:38)
Lean library rust integration? (181 messages, latest: Aug 23 2024 at 02:30)
lean cryptography library API for NIKE (34 messages, latest: Aug 21 2024 at 04:05)
Sorting has Θ(n log n) query complexity (6 messages, latest: Aug 17 2024 at 10:00)
To what extent is Lean4 itself verified? (14 messages, latest: Aug 14 2024 at 08:23)
Formalizing and verifying a regular experssion engine (17 messages, latest: Aug 11 2024 at 06:25)
help with proof for decreasing_by in natToBytes (7 messages, latest: Aug 04 2024 at 02:01)
UNSOUND workshop at SPLASH 2024 (3 messages, latest: Aug 03 2024 at 21:27)
what does it mean to prove the correctness of a program? (24 messages, latest: Jul 31 2024 at 06:45)
parser generators (3 messages, latest: Jul 30 2024 at 22:45)
SAIL to Lean (12 messages, latest: Jul 24 2024 at 12:37)
Beginner Resources for Program Verification in Lean ? (6 messages, latest: Jul 19 2024 at 14:43)
what advantages does lean have over f* and dafny? (11 messages, latest: Jul 18 2024 at 06:05)
channel events (1 message, latest: Jun 21 2024 at 01:35)
What is the status of program extraction? (17 messages, latest: Jun 17 2024 at 14:03)
Linear programming (57 messages, latest: Jun 04 2024 at 13:48)
State of affairs of verification of rust programs (3 messages, latest: Jun 03 2024 at 16:58)
Destructing fixed-length list (6 messages, latest: Apr 23 2024 at 15:16)
Port of Rocq's Deriving such that tactic (16 messages, latest: Apr 23 2024 at 07:16)
Elimination rules (74 messages, latest: Apr 19 2024 at 15:19)
Iris Lean Toolchain Upgrade (4 messages, latest: Feb 14 2024 at 21:20)
Proving termination/correctness of KMP helper (2 messages, latest: Jan 29 2024 at 09:42)
Abstracting Definitional Interpreters in lean (1 message, latest: Jan 11 2024 at 15:48)
Verification of functions using mutability (STRef) (10 messages, latest: Dec 16 2023 at 19:36)
✔ Using Parsec (14 messages, latest: Dec 15 2023 at 09:39)
How to approach proving termination here? (18 messages, latest: Nov 30 2023 at 15:16)
Formalizing a theoretical AI safety result (9 messages, latest: Nov 27 2023 at 13:25)
Help with a basic proof about Vectors (9 messages, latest: Nov 26 2023 at 20:29)
✔ Small-step operational semantics (70 messages, latest: Nov 25 2023 at 07:41)
Reflecting recursive types (1 message, latest: Oct 19 2023 at 12:54)
Stuck on proving a theorem about a simple program (4 messages, latest: Aug 13 2023 at 01:10)
Separation Logic (28 messages, latest: Jun 27 2023 at 13:55)
Functional Algorithms, Verified! (5 messages, latest: Jun 15 2023 at 17:27)
Verified program generation (17 messages, latest: Jun 14 2023 at 17:09)
RISC-V ISA in Lean (336 messages, latest: Apr 13 2023 at 10:12)
Representing proofs in Julia (1 message, latest: Apr 07 2023 at 07:56)
Infer a implementation of a blackbox function given table (10 messages, latest: Mar 30 2023 at 15:21)
Data structures (7 messages, latest: Jan 02 2023 at 12:00)
Generic State (17 messages, latest: Nov 30 2022 at 18:46)
executables (10 messages, latest: Oct 03 2022 at 22:16)
universes (33 messages, latest: Oct 15 2021 at 18:30)
Formal verification of simple imperative language (16 messages, latest: Jul 01 2021 at 13:50)
Lists Without Duplicates (84 messages, latest: Jan 01 2021 at 18:50)
lawful parsers (47 messages, latest: Dec 13 2020 at 00:28)
Quantum Computing (15 messages, latest: Dec 10 2020 at 13:08)
Examples (3 messages, latest: Nov 24 2020 at 17:14)
Working with match expression (7 messages, latest: Nov 01 2020 at 00:04)
Verifying 2-3 trees (1 message, latest: Oct 29 2020 at 15:19)
Correctness of a compiler for arithmetic expressions (6 messages, latest: Oct 20 2020 at 00:47)
Problem with pattern matching in function definition (4 messages, latest: Sep 24 2020 at 22:14)
Why Lean? (9 messages, latest: Sep 21 2020 at 21:23)
API for Lean (7 messages, latest: Sep 16 2020 at 20:00)
Transition Systems (3 messages, latest: Sep 04 2020 at 16:20)
Bitvector (39 messages, latest: Aug 17 2020 at 12:15)
Arena allocation for ITPs (50 messages, latest: Aug 12 2020 at 10:04)
Need a way to unfold a definition (460 messages, latest: Jul 09 2020 at 01:24)
upper bounds on proof translation (18 messages, latest: Jul 01 2020 at 20:14)
How to deal with exploding number of cases? (8 messages, latest: Jun 28 2020 at 18:07)
Concrete semantics (7 messages, latest: Jun 27 2020 at 18:36)
Metamath C (1 message, latest: Jun 21 2020 at 03:14)
SMT (Z3) bindings (12 messages, latest: Jun 18 2020 at 21:37)
SF kata (33 messages, latest: Jun 13 2020 at 18:07)
Turing machines (31 messages, latest: May 24 2020 at 12:28)
design by contract with lean (2 messages, latest: May 04 2020 at 14:04)
stream events (8 messages, latest: May 03 2020 at 22:53)

Last updated: May 02 2025 at 03:31 UTC