违抗
发表于 2025-4-1 03:28:46
Abstract Local Reasoning for Program Modulesinstance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions throughout the proof.
Paraplegia
发表于 2025-4-1 07:22:58
From Corecursive Algebras to Corecursive Monadsproved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot’s iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.
wangle
发表于 2025-4-1 12:51:37
http://reply.papertrans.cn/16/1525/152485/152485_63.png
GNAT
发表于 2025-4-1 17:47:57
Refinement Trees: Calculi, Tools, and Applicationstegrated with other tools like model finders and conservativity checkers. This technique has already been applied for showing the consistency of a first-order ontology that is too large to be tackled directly by model finders.
murmur
发表于 2025-4-1 18:43:24
https://doi.org/10.1007/978-3-663-20338-4ypes to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules.
Throttle
发表于 2025-4-2 00:09:03
https://doi.org/10.1007/978-3-662-26471-3r second main result concerns a strong completeness result for M., provided that the functor . satisfies some additional constraints. Our proof for this result is based on the construction, for an M.-consistent set of formulas ., of a coalgebraic model in which . is satisfiable.