licence
发表于 2025-3-25 03:42:14
Chasing Bottomssting properties of programs in the presence of partial and infinite values. By testing before proving we avoid wasting time trying to prove statements that are not valid. Then we prove that the programs we have written are in fact (more or less) inverses using first fixpoint induction and then the approximation lemma.
强制令
发表于 2025-3-25 07:34:33
http://reply.papertrans.cn/63/6270/626965/626965_22.png
sleep-spindles
发表于 2025-3-25 13:39:05
Modelling Nondeterminisme.ned into functions that can be translated into an appropriate functional programming language. We now propose to go one step further, since the domain of relations can be used to describe only angelic or demonic nondeterminism, but not both.
abolish
发表于 2025-3-25 19:04:08
An Injective Language for Reversible Computationng a history. The language is presented with many examples, and its relationship with Bennett’s reversible Turing machine is explained. The language serves as a good model for program construction and reasoning for reversible computers, and hopefully for modelling bi-directional updating in an editor.
infatuation
发表于 2025-3-25 20:10:42
Prototyping Generic Programming in Template Haskellng languages, PolyP and Generic Haskell, using Template Haskell, an extension to Haskell that enables compile-time meta-programming. In doing this we also gain a better understanding of the differences and similarities between the two languages.
vasospasm
发表于 2025-3-26 02:27:44
Friends Need a Bit More: Maintaining Invariants Over Shared Staten exisiting ownership type systems because they link objects that are not in the same ownership domain. Friendship permits the modular verification of cooperating classes. This paper defines friendship, sketches a soundness proof, and provides several realistic examples.
贪婪地吃
发表于 2025-3-26 04:57:33
http://reply.papertrans.cn/63/6270/626965/626965_27.png
Perineum
发表于 2025-3-26 11:30:10
Transposing Relations: From , Functions to Hash Tablesble to simple relations only..Our illustration of the usefulness of the generic transpose takes advantage of the . of a polymorphic function. We show how to derive laws of relational combinators as free theorems of their transposes. Finally, we relate the topic of functional transposition with the . technique for efficient data representation.
Defiance
发表于 2025-3-26 15:55:10
Augmenting Types with Unbounded Demonic and Angelic Nondeterminacyminacy arises naturally in specification and programming languages, we speculate that it combines fruitfully with function theory to the extent that it can play an important role in facilitating proofs of programs that have no apparent connection with nondeterminacy.
Cirrhosis
发表于 2025-3-26 17:05:48
Pointer Theory and Weakest Preconditions without Addresses and Heaposition of them. Those ./.-definitions and the concept of trace equivalence are the result of the paper. They are intended as a foundation for program design; in particular, for an object-oriented one.