math-comp
[Paper Artifact] Application of s-finite kernels to program semantics
This PR is an application of s-finite kernels to probabilistic programs. (NB: an early version of this PR appeared as PR #749 which is scheduled for closing)
It provides a semantics, an intrinsically-typed syntax, and examples of verified programs.
The semantics and several examples are documented in https://dl.acm.org/doi/10.1145/3732291 [R. Affeldt, C. Cohen, A. Saito, Semantics of Probabilistic Programs Using s-Finite Kernels in Dependent Type Theory, ACM Trans. Probab. Mach. Learn, 2025] (which is a revised and extended version of a conference paper that was presented at CPP 2023 https://dl.acm.org/doi/10.1145/3573105.3575691).
Note that the hierarchy of kernels has been merged into master (see PR #896 and PR #1444)
The intrinsically-typed syntax and more examples are explained in [A. Saito, R. Affeldt, Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq, APLAS 2023].
@CohenCyril @AyumuSaito
File "./prob_lang.v", line 10, characters 0-33:
Error: Cannot find a physical path bound to logical path
lra with prefix mathcomp.
Isn't it just a matter of adding Algebra Tactics to the dependencies in the nix configuration?
Also, please consider fixing math-comp/algebra-tactics#62 before merging this.