Every coalgebra for a well-founded functor on a category of families indexed by a well-founded relation is recursive.
InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K
7 Pith papers cite this work. Polarity classification is still indexing.
7
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
roles
background 2polarities
background 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.
PaJAM generalizes JAM/IAM/PAM via backtracking depth and extracts its step count from non-idempotent intersection type derivations, yielding a polynomial reasonable cost model for bounded depth.
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.
A sound and complete deductive system for relative trace equality based on relative bisimulation is introduced, formalized in Rocq, and demonstrated on two contract satisfaction proofs.
A sound and complete prophecy-based reduction of message-passing program verification to CHC satisfiability is proposed, with a prototype implementation for Rust-like programs.
citing papers explorer
-
On Jumps, Interactions, and Intersection Types
PaJAM generalizes JAM/IAM/PAM via backtracking depth and extracts its step count from non-idempotent intersection type derivations, yielding a polynomial reasonable cost model for bounded depth.
-
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.
-
A Deductive System for Contract Satisfaction Proofs
A sound and complete deductive system for relative trace equality based on relative bisimulation is introduced, formalized in Rocq, and demonstrated on two contract satisfaction proofs.
-
Prophecy-Based Automated Verification of Message-Passing Programs
A sound and complete prophecy-based reduction of message-passing program verification to CHC satisfiability is proposed, with a prototype implementation for Rust-like programs.