Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq
Abstract elided by the publisher.
Related papers
- Semantics of Probabilistic Programs using s-Finite Kernels in Coq CPP 2023
- Decalf: A Directed, Effectful Cost-Aware Logical Framework POPL 2024
- The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier ICFP 2013
- A State-of-the-Art Karp-Miller Algorithm Certified in Coq TACAS 2024
- Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report) ICFP 2018
- Progressful Interpreters for Efficient WebAssembly Mechanisation POPL 2025
- Intrinsically-typed definitional interpreters for linear, session-typed languages CPP 2020
- Intrinsically-typed definitional interpreters à la carte OOPSLA 2022