Cerisier is the first mechanized program logic for modular reasoning about trusted, untrusted, and attested code in capability machines, with a universal contract for untrusted code and demonstrations on secure computation and mutual attestation.
Iris from the ground up
7 Pith papers cite this work, alongside 368 external citations. Polarity classification is still indexing.
7
Pith papers citing it
368
external citations · OpenAlex
citation-role summary
method 2
citation-polarity summary
roles
method 2polarities
use method 2representative citing papers
Foxtrot is the first higher-order separation logic for contextual refinement of higher-order concurrent probabilistic programs with higher-order local state, mechanized in Rocq and Iris.
Contravariant families in simplicial HoTT supply proof-relevant expansion, yielding directed Boolean canonicity and a binary parametricity model over reduction-aware syntax.
Continuous-Eris is a new separation logic that verifies exact samplers for the uniform, Gaussian, and Laplace distributions plus an exact real arithmetic library, with all proofs machine-checked in Rocq.
Constructs a logical-relations security model for where-declassification in higher-order languages by halting indistinguishability enforcement after relevant declassifications, yielding stronger guarantees than prior lower-order definitions.
Semantic typing via coinductively defined interpretations on a typed operational semantics ensures information flow control and non-interference for TinySol contracts that use fallback functions.
Generalizes rely-guarantee to parametric memory models and presents Piccolo, the first such logic for causally consistent shared memory using potential-based operational semantics.
citing papers explorer
-
Cerisier: A Program Logic for Attestation in a Capability Machine
Cerisier is the first mechanized program logic for modular reasoning about trusted, untrusted, and attested code in capability machines, with a universal contract for untrusted code and demonstrations on secure computation and mutual attestation.
-
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Foxtrot is the first higher-order separation logic for contextual refinement of higher-order concurrent probabilistic programs with higher-order local state, mechanized in Rocq and Iris.
-
Directed proof-relevant logical relations in simplicial HoTT
Contravariant families in simplicial HoTT supply proof-relevant expansion, yielding directed Boolean canonicity and a binary parametricity model over reduction-aware syntax.
-
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
Continuous-Eris is a new separation logic that verifies exact samplers for the uniform, Gaussian, and Laplace distributions plus an exact real arithmetic library, with all proofs machine-checked in Rocq.
-
Compositional security definitions for higher-order where declassification
Constructs a logical-relations security model for where-declassification in higher-order languages by halting indistinguishability enforcement after relevant declassifications, yielding stronger guarantees than prior lower-order definitions.
-
Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts
Semantic typing via coinductively defined interpretations on a typed operational semantics ensures information flow control and non-interference for TinySol contracts that use fallback functions.
-
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
Generalizes rely-guarantee to parametric memory models and presents Piccolo, the first such logic for causally consistent shared memory using potential-based operational semantics.