Cryptic
发表于 2025-3-30 12:13:16
http://reply.papertrans.cn/23/2226/222555/222555_51.png
ARIA
发表于 2025-3-30 13:10:31
Tail recursion from universal invariants,eting tail recursion by means of the colimit of a loop diagram, i.e. its universal invariant. Parametrised initial algebras always have universal invariants, while the converse holds in the presence of equalisers..Consequences include categorical descriptions of vectors and matrices, which allow def
健壮
发表于 2025-3-30 20:26:15
http://reply.papertrans.cn/23/2226/222555/222555_53.png
Alienated
发表于 2025-3-30 23:01:44
Constructions and predicates,ints: (1) a simple new operation is added — to represent a constructive version of the .; (2) a restriction on contexts is imposed — "sets" must not depend on "proofs" of "predicates". The resulting theory is called .. Sufficiently constructive arguments from naive set theory can be directly written
anus928
发表于 2025-3-31 04:23:38
Relating models of impredicative type theories,onstructions and Higher Order ML. The latter is particularly interesting because it is a two-level type theory with type dependency at both levels. Having described appropriate categorical structures for these calculi, we establish translations back and forth between all of them. Most of the researc
叫喊
发表于 2025-3-31 08:57:50
http://reply.papertrans.cn/23/2226/222555/222555_56.png
callous
发表于 2025-3-31 12:46:20
An algebra of graphs and graph rewriting,ay be interpreted as graphs having both a concrete part and an abstract part (defined up to isomorphism). Morphisms between pa-graphs are pushout squares. We show that the basic notions of the algebraic theory of graph grammars (instantiated to a suitable category of graphs) can be rephrased
HEPA-filter
发表于 2025-3-31 17:26:42
http://reply.papertrans.cn/23/2226/222555/222555_58.png
性冷淡
发表于 2025-3-31 20:55:57
Applications of the calculus of trees to process description languages,te concurrent calculus. Then, suitable motors that constructively define canonical representatives for strong and observational congruence based on the notion of bisimulation are introduced in a clean and straightforward way. This enables us to provide the calculus with a fully abstract semantics up