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
5 Pith papers cite this work. Polarity classification is still indexing.
5
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.
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.
FM-Agent is the first framework to automate compositional Hoare reasoning for large systems by having LLMs derive natural-language function specs from caller intent and then generate tests that found 522 new bugs in systems up to 143k lines of code.
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.
citing papers explorer
-
Intrinsically Correct Algorithms and Recursive Coalgebras
Every coalgebra for a well-founded functor on a category of families indexed by a well-founded relation is recursive.
-
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.
-
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.
-
FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning
FM-Agent is the first framework to automate compositional Hoare reasoning for large systems by having LLMs derive natural-language function specs from caller intent and then generate tests that found 522 new bugs in systems up to 143k lines of code.
-
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.