Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
5 results

Codensity Lifting of Monads and its Dual

Shin-ya Katsumata ; Tetsuya Sato ; Tarmo Uustalu.
We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations which were not supported by its precursor, categorical TT-lifting. After introducing the codensity lifting, we illustrate&nbsp;[&hellip;]
Published on October 29, 2018
Volume 14, Issue 4

When is a container a comonad?

Danel Ahman ; James Chapman ; Tarmo Uustalu.
Abbott, Altenkirch, Ghani and others have taught us that many parameterized datatypes (set functors) can be usefully analyzed via container representations in terms of a set of shapes and a set of positions in each shape. This paper builds on the observation that datatypes often carry additional&nbsp;[&hellip;]
Published on September 3, 2014
Volume 10, Issue 3

Monads need not be endofunctors

Thosten Altenkirch ; James Chapman ; Tarmo Uustalu.
We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore&nbsp;[&hellip;]
Published on March 6, 2015
Volume 11, Issue 1

On streams that are finitely red

Marc Bezem ; Keiko Nakata ; Tarmo Uustalu.
Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing&nbsp;[&hellip;]
Published on October 10, 2012
Volume 8, Issue 4

A Hoare logic for the coinductive trace-based big-step semantics of While

Keiko Nakata ; Tarmo Uustalu.
In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for While. In this semantics, both traces and evaluation (relating initial states of program runs to traces they produce) are&nbsp;[&hellip;]
Published on February 11, 2015
Volume 11, Issue 1
  • < Previous
  • 1
  • Next >