finalcoalgebra
Re:The brain may be about to have its Ozempic moment
on Tuesday August 11, 2026 @07:13PM (#49265763)
Wild to read this about your sleep pattern. Please explain more. I find myself needing to sleep like 12+ hours every day.
Re:Automatically Translating Proof Systems for SMT Solvers to the λΠ-C...
on Monday February 23, 2026 @07:47AM (#47121638)
Eunoia is an emerging logical framework for specifying the
proofs and proof systems of SMT solvers, namely CVC5. We present a
translation from Eunoia to the λΠ-calculus modulo rewriting as implemented
by the LambdaPi proof assistant. The translation is implemented by our
tool eo2lp, which we use for generating LambdaPi encodings of (a) a large
fragment of CVC5’s Cooperating Proof Calculus (CPC), and (b) proofs
produced by CVC5 on unsat problems from various fragments of SMT-LIB.