Formalizing a First-order Differentiable Logic with MathComp
summary
Claims a formalized, well-behaved first-order differentiable logic built on MathComp by extending its analysis libraries with a correct power function for extended reals and a formal proof of Hölder’s inequality for extended reals, giving P‑parametrized p‑norm semantics that approximate max/sup and integrals-as-quantifiers over probability spaces. Implements a sound sequent calculus (completeness work in progress), submits the fifth revision of the power function to upstream, and reports partial success integrating Hölder for extended reals and MathComp extension patches under review.
AI-written summary · about
chapters (5)
- 0:00Differentiable logics intro
- 3:35Soft Büchi Logic
- 7:05Calculus and proof theory
- 9:09MathComp formalization progress
- 10:33Q&A
related talks
30mλS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
49mSemantic Foundations for Probabilistic Programming
22mReasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence
22mA formalization of Doob's martingale convergence theorems in mathlib
30mAutomatic Differentiation in PCF
24mSemantics of Probabilistic Programs using S-Finite Kernels in Coq
23mA Framework of Differential Operators