Author name cluster

Varmo Vene

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

I&C Journal 2006 Journal Article

Recursive coalgebras from comonads

Venanzio Capretta
Tarmo Uustalu
Varmo Vene

The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the use of recursive coalgebras as a paradigm of structured recursion in programming semantics, list some basic facts about recursive coalgebras and, centrally, give new conditions for the recursiveness of a coalgebra based on comonads, comonad-coalgebras and distributive laws of functors over comonads. We also present an alternative construction using countable products instead of cofree comonads.

Details DOI

TCS Journal 2006 Journal Article

Type systems equivalent to data-flow analyses for imperative languages

Peeter Laud
Tarmo Uustalu
Varmo Vene

We show that a large class of data-flow analyses for imperative languages are describable as type systems in the following technical sense: possible results of an analysis can be described in a language of types so that a program checks with a type if and only if this type is a supertype of the result of applying the analysis. Type-checking is easy with the help of a certificate that records the “eureka”-bits of a typing derivation. Certificate-assisted type-checking amounts to a form of lightweight analysis à la Rose. For secure information flow, we obtain a type system that is considerably more precise than that of Volpano et al. , but not more sophisticated. Importantly, our type systems are compositional.

Details DOI

TCS Journal 2002 Journal Article

Least and greatest fixed points in intuitionistic natural deduction

Tarmo Uustalu
Varmo Vene

This paper is a comparative study of a number of (intensional-semantically distinct) least and greatest fixed point operators that natural-deduction proof systems for intuitionistic logics can be extended with in a proof-theoretically defendable way. Eight pairs of such operators are analysed. The exposition is centred around a cube-shaped classification where each node stands for an axiomatization of one pair of operators as logical constants by intended proof and reduction rules and each arc for a proof- and reduction-preserving encoding of one pair in terms of another. The three dimensions of the cube reflect three orthogonal binary options: conventional-style vs. Mendler-style, basic (“[co]iterative”) vs. enhanced (“primitive–[co]recursive”), simple vs. course-of-value [co]induction. Some of the axiomatizations and encodings are well known; others, however, are novel; the classification into a cube is also new. The differences between the least fixed point operators considered are illustrated on the example of the corresponding natural number types.

Details DOI