Titlebook: Mathematics of Program Construction; 7th International Co Dexter Kozen Conference proceedings 2004 Springer-Verlag Berlin Heidelberg 2004 D

fibula

Constituent

Constructing Polymorphic Programs with Quotient Typesrphism has been one of the most successful approaches to date but, as of yet, has not been applicable to programming with quotient datatypes such as unordered pairs, cyclic lists, bags etc. This paper provides the basis for writing polymorphic programs over quotient datatypes by extending our recent

闪光东本

Optimizing Generic Functionsne acquires this operation over any particular type. An instance on a specific type is generated by interpretation of the type’s structure. A direct translation leads to extremely inefficient code that involves many conversions between types and their structural representations. In this paper we pre

Diatribe

Inferring Type Isomorphisms Genericallypair of binary products. In some canonical cases, the conversion function is uniquely determined solely by the two types involved. In this article we describe and implement a program in Generic Haskell which automatically infers this function by normalizing types w.r.t. an algebraic theory of canoni

文件夹

Friends Need a Bit More: Maintaining Invariants Over Shared Stateefined. Friendship is a flexible protocol that allows invariants expressed over shared state. Such invariants are more expressive than those allowed in exisiting ownership type systems because they link objects that are not in the same ownership domain. Friendship permits the modular verification of

Circumscribe

滑动

Describing Gen/Kill Static Analysis Techniques with Kleene Algebra, we formalize four instances of a static data flow analysis technique known as gen/kill analysis. This formalization clearly reveals the dualities between the four instances; although these dualities are known, the standard formalization does not reveal them in such a clear and concise manner. We p

Agronomy

A Free Construction of Kleene Algebras with Tests free Kleene algebra with tests generated by a pair of sets. We also show that the category . of Kleene algebras with tests and the category .. of Kozen’s Kleene algebras with tests are related by an adjunction. This fact shows that an infinitely-generated free Kleene algebra with tests in the sense

ALLEY

Streaming Representation-Changersld after a fold; typically, it will convert from one data representation to another. In general, metamorphisms are less interesting than hylomorphisms: there is no automatic . to . the intermediate virtual data structure. However, under certain conditions fusion is possible: some of the work of the

去世