Kleene Coalgebra

Computing with Capsules

A capsule is a pair (e,t), where e is a lambda-term and t is a partial function with finite domain from variables to irreducible lambda-terms (irreducible = constant or lambda-abstraction, not a variable!) such that (1) for all x in dom t, FV(t(x)) subset dom t, and (2) FV(e) subset dom t.  Capsules provide a simple algebraic representation of the state of a computation in higher-order functional and imperative languages.  They can be used to model closures or heap-allocated environments but are much simpler than either.  A capsule is essentially a finite coalgebra representing a (possibly infinite) regular closed lambda-coterm.  Recursive functions are represented directly as such coterms without using a fixpoint combinator, and all operations are typable with simple types, yet the system is Turing complete.  Thus we can avoid the use of unnatural fixpoint combinators that are untypable with simple types and impose a call-by-name discipline.  In this talk I will describe a simple functional/imperative programming language based on capsules, give a large-step operational semantics and a coinductive type inference algorithm, and show that the language adequately captures lexical scoping without stacks or closures.

(joint work with Jean-Baptiste Jeannin, Cornell)

A coalgebraic perspective on logical interpretation

Luis Soares Barbosa, Universidade do Minho

In Computer Science, stepwise refinement of algebraic specifications is a well known formal methodology for rigorous program development. This talk illustrates how techniques from Algebraic Logic, in particular the notion of interpretation, understood as a multifunction that preserves and reflects logical consequence, captures a number of relevant transformations in the context of software design difficult to deal with in classical approaches. Examples include data encapsulation and the decomposition of operations into atomic transactions. But if interpretations open such a new research avenue in program refinement, (conceptual) tools are needed to reason about them. Therefore, we will also discuss a correspondence between logical interpretations and morphisms for a particular kind of coalgebras, so that usual coalgebraic constructions, such as bisimulation, can be used to reason about interpretations between (abstract) logics.

Beyond Kleene Coalgebra

Alexandra Silva, Centrum Wiskunde & Informatica,  Amsterdam, NL

In this talk, I will present an overview of the results conatined in my thesis “Kleene 

Coalgebra” and will discuss future research directions.