不易燃
发表于 2025-3-28 18:37:41
Primitive recursive functional with dependent types, with primitive recursion and a simple type system with primitive recursive sequences of types and products dependent on natural numbers. I show that it is possible in this system, called .., to type a sensible primitive recursive function that is not typable in ML. The paper presents typing rules,
轻浮女
发表于 2025-3-28 20:58:53
Typed homomorphic relations extended with subtypes,Such relations are needed for the model theory of incomplete, hierarchical specifications with subtypes. Typed logical relations are generalized similarly. These tools help give a simple model-theoretic account of subtyping among abstract data types as observed by terms of a simply-typed lambda-calc
揭穿真相
发表于 2025-3-29 02:53:14
http://reply.papertrans.cn/63/6262/626161/626161_43.png
Lipohypertrophy
发表于 2025-3-29 04:23:12
http://reply.papertrans.cn/63/6262/626161/626161_44.png
Infiltrate
发表于 2025-3-29 10:42:55
HSP type theorems in the category of posets,ories depends on what is meant by subobject. The correspondence between subcategories does not hold as it does in sets, primarily because the axiom of choice (in the form that epimorphisms split) totally fails in posets. Although equations, suitably generalized to include inequalities, determine HSP
ESO
发表于 2025-3-29 13:09:19
Cartesian closed categories of domains and the space proj(D), If . is a full cartesian closed subcategory of ALG. such that . is closed under . → ., then every object . is ., i.e., im(.) is algebraic for all . ∃ .. This is equivalent to assuming that all order-dense chains in K(.) are degenerate. If . contains an isomorphic copy of the flat natural numbers, t
abstemious
发表于 2025-3-29 17:01:46
An upper power domain construction in terms of strongly compact sets,sets, but still admit all necessary operations, i.e. they contain less junk. The notion of strong compactness allows a proof of stronger properties than compactness would, e.g. an intrinsic universal property of the upper power construction, and its commutation with the lower construction.
cruise
发表于 2025-3-29 19:57:04
http://reply.papertrans.cn/63/6262/626161/626161_48.png
有限
发表于 2025-3-29 23:55:47
An algorithm for analyzing communicating processes,ons between processes. Some static analysis methods have been developed to determine how processes are synchronised, but all the algorithms proposed until now are exponential. This paper presents, for CSP-like programs, a static and automatic analysis algorithm using abstract interpretation and base
性满足
发表于 2025-3-30 04:48:25
http://reply.papertrans.cn/63/6262/626161/626161_50.png