抛物线 发表于 2025-3-25 06:54:51
http://reply.papertrans.cn/43/4270/426989/426989_21.pngacolyte 发表于 2025-3-25 09:16:10
https://doi.org/10.1007/3-540-61254-8Addition; Graph Rrewriting; Graphersetzung; Higher-Order Algebra; Higher-Order Logic; Higher-Order Term; HFoment 发表于 2025-3-25 13:39:07
http://reply.papertrans.cn/43/4270/426989/426989_23.pngDiaphragm 发表于 2025-3-25 17:33:51
Modular properties of algebraic type systems,ate a generic study of the modular properties of these systems. We give a general criterion for one system of this framework to be strongly normalising. As an application of our criterion, we recover all previous strong normalisation results for algebraic type systems.GRACE 发表于 2025-3-25 22:05:31
Collapsing partial combinatory algebras,n this paper we develop some general theory concerning homomorphic images (or collapses) of pca‘s, obtained by identification of elements in a pca. We establish several facts concerning final collapses (maximal identification of elements). ‘En passant’ we find another example of a pca that cannot be代理人 发表于 2025-3-26 03:21:05
http://reply.papertrans.cn/43/4270/426989/426989_26.pngmonopoly 发表于 2025-3-26 07:51:22
- and ,-logics,g upon Russell‘s ramified theory of types, we develop the theory of ..-logics, which are axiomatisable by an order-sorted equational Horn logic with a membership predicate, and of ..-logics, that provide in addition partial functions. The latter are therefore more adapted to the use in the program sULCER 发表于 2025-3-26 11:22:59
The variable containment problem, of .-terms rather than .-terms themselves, as for instance in higher-order rewriting. An important problem for (generalised) higher-order rewrite systems is the .: given two terms . and ., do we have for all substitutions . and contexts .[]that FV.(..).FV.(.[..])?.This property is important when wearthroplasty 发表于 2025-3-26 14:04:15
Higher-order equational logic for specification, simulation and testing,s on the expressiveness and proof theory of higher-order equations. These results are then interpreted within the context of specification language design to show that higher-order equational logic, used as a specification language, provides a useful compromise between the conflicting requirements o难取悦 发表于 2025-3-26 17:03:03
The correctness of a higher-order lazy functional language implementation: An exercise in mechanicartunate side-effect of the improved efficiency is the increasing complexity of the resultant implementations. In this paper we present the correctness proof of a new abstract machine. The abstract machine deals with the issues of currying, nonstrictness and sharing. Like most modern abstract machine