Affordable Access

Publisher Website

Monads, Effects and Transformations

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
26
Identifiers
DOI: 10.1016/s1571-0661(05)80280-4
Disciplines
  • Computer Science
  • Logic
  • Mathematics

Abstract

Abstract We define a typed compiler intermediate language, MIL-lite, which incorporates computational types refined with effect information. We characterise MIL-lite observational congruence by using Howe's method to prove a ciu theorem for the language in terms of a termination predicate defined directly on the term. We then define a logical predicate which captures an observable version of the intended meaning of each of our effect annotations. Having proved the fundamental theorem for this predicate, we use it with the ciu theorem to validate a number of effect-based transformations performed by the MLj compiler for Standard ML.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

Substitution: A formal methods case study using mo...

on Science of Computer Programmin... Jan 01, 1994

Hopf monads

Apr 26, 2006
More articles like this..