Evidence-tracked tape semantics yields a higher-order logic for randomized programs in which entailments are witnessed by uniform evidence transformers and quantitative probabilities arise by interpretation under a chosen tape measure.
Semantics of probabilistic programs.Journal of Computer and System Sciences, 22(3):328–350
3 Pith papers cite this work, alongside 507 external citations. Polarity classification is still indexing.
3
Pith papers citing it
507
external citations · Crossref
citation-role summary
method 1
citation-polarity summary
fields
cs.LO 3roles
method 1polarities
use method 1representative citing papers
Introduces a trust-boundary architecture in Lean 4 with three certificate families and two operators that deliver sorry-free, axiom-audited assurances for LLM pipeline components.
A while-language with differential equations and random sampling is given an operational semantics, a denotational semantics, and an adequacy theorem relating the two.
citing papers explorer
-
Evidence-Tracked Tape Semantics for Probabilistic Computation
Evidence-tracked tape semantics yields a higher-order logic for randomized programs in which entailments are witnessed by uniform evidence transformers and quantitative probabilities arise by interpretation under a chosen tape measure.
-
Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
Introduces a trust-boundary architecture in Lean 4 with three certificate families and two operators that deliver sorry-free, axiom-audited assurances for LLM pipeline components.
-
An Adequate While-Language for Stochastic Hybrid Computation
A while-language with differential equations and random sampling is given an operational semantics, a denotational semantics, and an adequacy theorem relating the two.