Open Research Index

Coinductive reasoning for parametrized functors and monads

Ugo Dal Lago, Zeinab Galal

arXivarxiv/2609.35691Sep 28, 2026cs.LOscore 0

Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2609.35691
curl -X POST /api/v1/records/arxiv/2609.35691/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.35691/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'