Monadic effects and equational reasoning in Rocq
-
Updated
Jul 21, 2026 - Rocq Prover
Monadic effects and equational reasoning in Rocq
A library for testing concurrent C++ code and deterministically reproducing bugs.
A fast and dirty checker based on libclang which detects non-deterministic iteration
For our ASE20 paper 🏆 "Problems and Opportunities in Training Deep Learning Software Systems: An Analysis of Variance" by Hung Viet Pham, Shangshu Qian, Jiannan Wang, Thibaud Lutellier, Jonathan Rosenthal, Lin Tan, Yaoliang Yu, and Nachiappan Nagappan. (🏆 Distinguished Paper Award!)
For our NeurIPS21 paper "Are My Deep Learning Systems Fair? An Empirical Study of Fixed-Seed Training" by Shangshu Qian, Hung Viet Pham, Thibaud Lutellier, Zeou Hu, Jungwon Kim, Lin Tan, Yaoliang Yu, Jiahao Chen, and Sameena Shah
Finite state automata and regular expressions. Context-free grammars and pushdown automata. Turing machines. Models of computable functions and undecidable problems. The course emphasis is on the theory of computability, especially on showing limits of computation. May be taken for graduate credit.
For our ASE21 tool paper "DEVIATE: A Deep Learning Variance Testing Framework" by Hung Viet Pham, Mijung Kim, Lin Tan, Yaoliang Yu, and Nachiappan Nagappan.
A Python library for nondeterministic algorithms
Monad instances for a rose-tree-like data structure used for nondeterministic computations.
An AI-powered LLM output consistency / nondeterminism profiler - runs a prompt K times, measures output variance across runs, and flags flaky/unreliable prompts before they ship. Provider-agnostic, BYO-key, offline --dry-run. Python CLI.
Float accumulation order alone flips RL reward verdicts and sampler/trainer probabilities — reproduce it on real GPT-2, then remove it with an order-independent reduction. numpy-only, runs in seconds.
同じコードをローカルLLM(Qwen2.5-Coder/Ollama)にN回監査させたときの指摘の揺れ(反復非決定性)と多数決の落とし穴を実測する再現キット。二層再現:生成ログ凍結+決定的集計。
Find the exact line where a JVM program stops being reproducible.
Material suplementar do TCC "Reprodutibilidade da inferência de LLMs sob carga" (MBA USP/ESALQ, 2026): rotina de coleta e análise do experimento de não determinismo em inferência sob carga concorrente.
The infinite unnecessary expansion, Negative Zero
Run a function in fresh processes and see if it answers the same. A witness is a fact; agreement is not.
Runs a batch pipeline several times and reports, per step, how often it failed to give the same answer. Distinguishes real nondeterminism from float noise.
To associate your repository with the nondeterminism topic, visit your repo's landing page and select "manage topics."