Reservation
发表于 2025-3-30 08:14:58
http://reply.papertrans.cn/43/4270/426990/426990_51.png
Cryptic
发表于 2025-3-30 14:57:50
Prototyping relational specifications using higher-order objects,n-algebraic descriptions of higher-order objects. From non-constructive characterizations executable relational specifications are obtained. We also show how to develop more efficient algorithms from the frequently inefficient specifications within the calculus of binary relations.
出血
发表于 2025-3-30 19:09:22
Origin tracking for higher-order term rewriting systems, of subterms, the ., in the initial term. Origin tracking is based on the notion of residuals. It has been used successfully for the generation of error handlers and debuggers from algebraic specifications of programming languages. Recent experiments with the use of higher-order algebraic specificat
植物学
发表于 2025-3-30 21:18:04
Theory interpretation in simple type theory,nce as well as in logic itself. This paper presents a method for theory interpretation in a version of simple type theory, called ., which admits partial functions and subtypes. The method is patterned on the standard approach to theory interpretation in first-order logic. Although the method is bas
多余
发表于 2025-3-31 01:22:32
The semantics of SPECTRUM,n calculus and a development methodology. An informal presentation of the . language with many examples illustrating its properties is given in . The purpose of this article is to describe its formal semantics.
轻快带来危险
发表于 2025-3-31 05:47:11
: A typed language for algebraic specification, abstract types and combinators developed in Meinke . The system is intended to support the execution of equational specifications of abstract types and combinators. The type checking algorithms of the system also allow it to function as a framework for defining logics and proof checkin
蜈蚣
发表于 2025-3-31 10:59:52
http://reply.papertrans.cn/43/4270/426990/426990_57.png
散步
发表于 2025-3-31 15:12:48
Specification and verification in higher order algebra: A case study of convolution, systolic synchronous concurrent algorithms (SCAs) for convolution are formally specified and verified using higher order equational logic. We then study the metamathematics of these verification proofs by means of non-standard models.
anniversary
发表于 2025-3-31 21:24:49
http://reply.papertrans.cn/43/4270/426990/426990_59.png
CLEAR
发表于 2025-4-1 00:52:02
Comparing combinatory reduction systems and higher-order rewrite systems,fined by Nipkow. Although it always has been obvious that both formats are closely related to each other, up to now the exact relationship between them has not been clear. This was an unsatisfying situation since it meant that proofs for much related frameworks were given twice. We present two trans