描绘
发表于 2025-3-28 15:31:59
Unfolding Abstract Datatypes,s for . programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with solutions to two problems the solution to a problem in the recent literature.
量被毁坏
发表于 2025-3-28 18:45:26
Circulations, Fuzzy Relations and Semirings, directed from a source to a sink. We give a new description of circulations in networks using a technique introduced by Kawahara; he applied the same methods to network flows. We show the power and flexibility of his approach in a new application, refining it at the same time by introducing the con
的事物
发表于 2025-3-29 01:26:20
Asynchronous Exceptions as an Effect,interrupts underscores the importance of developing programming models to aid the development and verification of interrupt-driven programs. The research reported here recognizes asynchronous interrupts as a computational effect and encapsulates them as a building block in modular monadic semantics.
蛰伏
发表于 2025-3-29 06:54:22
,The Böhm–Jacopini Theorem Is False, Propositionally,is equivalent to a . program. The theorem is usually formulated at the first-order interpreted or first-order uninterpreted (schematic) level, because the construction requires the introduction of auxiliary variables. Ashcroft and Manna (1972) and Kosaraju (1973) showed that this is unavoidable. As
仔细阅读
发表于 2025-3-29 07:55:00
http://reply.papertrans.cn/63/6270/626958/626958_45.png
赦免
发表于 2025-3-29 12:56:49
Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representatihe argument types of the constructors refer to indices given by expressions where the family name may occur. Especially in this case of true nesting, there is no direct support by theorem provers to guarantee termination of functions that traverse these data structures..A joint article with A. Abel
incarcerate
发表于 2025-3-29 16:51:58
http://reply.papertrans.cn/63/6270/626958/626958_47.png
A保存的
发表于 2025-3-29 20:30:38
Algebra of Programming Using Dependent Types,he proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation
陈旧
发表于 2025-3-30 02:25:01
Safe Modification of Pointer Programs in Refinement Calculus, separation logic and then introduce a pair of new predicate transformers, called . and .. The new predicate transformers are derived from separating conjunction and separating implication, which are fundamental logical connectives in separation logic. They represent primitive forms of heap allocati
锯齿状
发表于 2025-3-30 05:28:10
A Hoare Logic for Call-by-Value Functional Programs,phic type system in the style of Hindley and Milner. It is the theoretical basis for a tool that extracts proof obligations out of programs annotated with logical assertions. These proof obligations, expressed in a typed, higher-order logic, are discharged using off-the-shelf automated or interactiv