arXiv:1501.05425v1 [] 22 Jan 2015

Foundational Extensible Corecursion
Jasmin Christian Blanchette

Andrei Popescu

Dmitriy Traytel

Inria Nancy & LORIA, France
Max-Planck-Institut für Informatik,
Saarbrücken, Germany

Department of Computer Science,
School of Science and Technology,
Middlesex University, UK

Technische Universität München,
Germany

jablanch@inria.fr

a.popescu@mdx.ac.uk

Abstract

falls within this fragment, since each call to natsFrom produces
one constructor before entering the nested call. Not only is the
equation consistent, it also fully specifies the function’s behavior.
The above definition is legitimate only if objects are allowed
to be infinite. This may be self-evident in a nonstrict functional
language such as Haskell, but in a total setting we must carefully distinguish between the well-founded inductive (or algebraic)
datatypes and the non-well-founded coinductive (or coalgebraic)
datatypes—often simply called datatypes and codatatypes, respectively. Recursive functions consume datatype values, peeling off a
finite number of constructors as they proceed; corecursive functions produce codatatype values, consisting of finitely or infinitely
many constructors. And in the same way that induction is available
as a proof principle to reason about datatypes and terminating recursive functions, coinduction supports reasoning over codatatypes
and productive corecursive functions.
Despite their reputation for esotericism, codatatypes have an
important role to play in both the theory and the metatheory of
programming. On the theory side, they allow a direct embedding
of a large class of nonstrict functional programs in a total logic.
In conjunction with interactive proofs and code generators, this
enables certified functional programming [10]. On the metatheory
side, codatatypes conveniently capture infinite, possibly branching
processes. Major proof developments rely on them, including those
associated with a C compiler [33], a Java compiler [34], and the
Java memory model [35].
Codatatypes are supported by an increasing number of proof
assistants, including Agda, Coq, Isabelle/HOL, Isabelle/ZF, Matita,
and PVS. They are also present in the CoALP dialect of logic
programming and in the Dafny specification language. But the
ability to introduce codatatypes is not worth much without adequate
support for defining meaningful functions that operate on them. For
most systems, this support can be characterized as work in progress.
The key question they all must answer is: What right-hand sides
can be safely allowed in a function definition?
Generally, there are two main approaches to support recursive
and corecursive functions in a proof assistant or similar system:

This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to
and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under wellbehaved operations, including constructors. Corecursive functions
that are well behaved can be registered as such, thereby increasing
the corecursor’s expressiveness. The metatheory is formalized in
the Isabelle proof assistant and forms the core of a prototype tool.
The corecursor is derived from first principles, without requiring
new axioms or extensions of the logic.
Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about
Programs—Mechanical verification; F.4.1 [Mathematical Logic
and Formal Languages]: Mathematical Logic—Mechanical theorem proving, Model theory
General Terms Algorithms, Theory, Verification
Keywords (Co)recursion, parametricity, proof assistants,
higher-order logic, Isabelle

1.

traytel@in.tum.de

Introduction

Total functional programming is a discipline that ensures computations always terminate. It is invaluable in a proof assistant, where
nonterminating definitions such as f x = f x + 1 can yield contradictions. Hence, most assistants will accept recursive functions only if
they can be shown to terminate. Similar concerns arise in specification languages and verifying compilers.
However, some processes need to run forever, without their
being inconsistent. An important class of total programs has been
identified under the heading of productive coprogramming [1, 7,
51]: These are functions that progressively reveal parts of their
(potentially infinite) output. For example, given a type of infinite
streams constructed by SCons, the definition

The intrinsic approach: A syntactic criterion is built into the
logic: termination for recursive specifications, productivity (or
guardedness) for corecursive specifications. The termination or
productivity checker is part of the system’s trusted code base.

natsFrom n = SCons n (natsFrom (n + 1))

The foundational approach: The (co)recursive specifications are
reduced to a fixpoint construction, which permits a simple definition of the form f = . . . , where f does not occur in the righthand side. The original equations are derived as theorems from
this internal definition, using dedicated proof tactics.
Systems favoring the intrinsic approach include the proof assistants
Agda and Coq, as well as tools such as CoALP and Dafny. The
main hurdle for their users is that syntactic criteria are inflexible;

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2015/1/23

This extensible corecursor gracefully handles codatatypes with
nesting through arbitrary type constructors (e.g., for infinite-depth
Rose trees nested through finite or infinite lists). Thanks to the
framework’s modularity, function specifications can combine corecursion with recursion, yielding quite expressive mixed fixpoint
definitions (Section 4). This is inspired by the Dafny tool, but our
approach is semantically founded and hence provably consistent.
The complete metatheory is implemented in Isabelle/HOL, as a
combination of a generic proof development parameterized by arbitrary type constructors and a tool for instantiating the metatheory
to user-specified instances (Section 5, [13]).
Techniques such as corecursion and coinduction up-to have
been known for years in the process algebra community, before
they were embraced and perfected by category theorists (Section 6).
This work is part of a wider program aiming at bringing insight
from category theory into proof assistants [12, 49]. The main contributions of this paper are the following:

the specification must be massaged so that it falls within a given
syntactic fragment, even though the desired property (termination
or productivity) is semantic. But perhaps more troubling in systems
that process theorems, soundness is not obvious at all and very
tedious to ensure; as a result, there is a history of critical bugs
in termination and productivity checkers, as we will see when we
review related work (Section 6). Indeed, Abel [2] observed that
Maybe the time is ripe to switch to a more semantical notion
of termination and guardedness. The syntactic guard condition gets you somewhere, but then needs a lot of extensions
and patching to work satisfactory in practice. Formal verification of it becomes too difficult, and only intuitive justification is prone to errors.
In contrast to Agda and Coq, proof assistants based on higherorder logic (HOL), such as HOL4, HOL Light, and Isabelle/HOL,
generally adhere to the foundational approach. Their logic is expressive enough to accommodate the (co)algebraic constructions
underlying (co)datatypes and (co)recursive functions in terms of
functors on the category of sets [49]. The main drawback of this
approach is that it requires a lot of work, both conceptual and implementational. Moreover, it is not available for all systems, since
it requires an expressive enough logic.
Because every step must be formally justified, foundational
definitional principles tend to be simpler and more restrictive than
their intrinsic counterparts. As a telling example, codatatypes were
introduced in Isabelle/HOL only recently, almost two decades after
their inception in Coq, and they are still missing from the other
HOL systems; and corecursion is limited to the primitive case, in
which corecursive calls occur under exactly one constructor.
That primitive corecursion (or the slightly extended version
supported by Coq) is too restrictive is an observation that has been
made repeatedly by researchers who use corecursion in Coq and
now also Isabelle. Lochbihler and Hölzl dedicated a paper [36] to
ad hoc techniques for defining operations on corecursive lists in
Isabelle. Only after introducing a lot of machinery do they manage
to define their central example—lfilter, a filter function on lazy
(coinductive) lists—and derive suitable reasoning principles.
We contend that it is possible to combine advanced features
as found in Agda and Coq with the fundamentalism of Isabelle.
The lack of built-in support for corecursion, an apparent weakness,
reveals itself as a strength as we proceed to introduce rich notions of
corecursion, without extending the type system or adding axioms.
In this paper, we formalize a highly expressive corecursion
framework that extends primitive corecursion in the following
ways: It allows corecursive calls under several constructors; it allows well-behaved operators in the context around or between the
constructors and around the corecursive calls; importantly, it supports blending terminating recursive calls with guarded corecursive
calls. This general corecursor is accompanied by a corresponding,
equally general coinduction principle that makes reasoning about
it convenient. Each of the corecursor, mixed recursor–corecursor,
and the coinduction principle grow in expressiveness during the interaction with the user, by learning of new well-behaved contexts.
The constructions draw heavily from category theory.
Before presenting the technical details, we first show through
examples how a primitive corecursor can be incrementally enriched
to accept ever richer notions of corecursive call context (Section 2).
This is made possible by the modular bookkeeping of additional
structure for the involved type constructors, including a relator
structure. This structure can be exploited to prove parametricity
theorems, which ensure the suitability of operators as participants
to the call contexts, in the style of coinduction up-to. Each new
corecursive definition is a potential future participant (Section 3).

• We represent in higher-order logic an integrated framework for

recursion and corecursion able to evolve by user interaction.
• We identify a sound fragment of mixed recursive–corecursive

specifications, integrate it in our framework, and present several
examples that motivate this feature.
• We implement the above in Isabelle/HOL within an interactive

loop that maintains the recursive–corecursive infrastructure.
• We use this infrastructure to automatically derive many exam-

ples that are problematic in other proof assistants.
A distinguishing feature of our framework is that it does not
require the user to provide type annotations. On the design space,
it lies between the highly restrictive primitive corecursion and the
more bureaucratic up-to approaches such as clock variables [7, 15]
and sized types [3], combining expressiveness and ease of use. The
identification of this “sweet spot” can also be seen as a contribution.

2.

Motivating Examples

We demonstrate the expressiveness of the corecursor framework
by examples, adopting the user’s perspective. The case studies by
Rutten [46] and Hinze [21] on stream calculi serve as our starting
point. Streams of natural numbers can be defined as
codatatype

Stream = SCons (head : Nat) (tail : Stream)

where SCons : Nat → Stream → Stream is the constructor and
head : Stream → Nat, tail : Stream → Stream are its selectors.
Although the examples may seem simple or contrived, they were
carefully chosen to show the main difficulties that arise in practice.
2.1

Corecursion Up-to

As our first example of a corecursive function definition, we consider the pointwise sum of two streams:
xs ⊕ ys = SCons (head xs + head ys) (tail xs ⊕ tail ys)
The specification is productive, since the corecursive call occurs
directly under the stream constructor, which acts as a guard (shown
underlined). Moreover, it is primitively corecursive, because the
topmost symbol on the right-hand side is a constructor and the
corecursive call appears directly as an argument to it.
These syntactic restrictions can be relaxed to allow conditional
statements and ‘let’ expressions [12], but despite such tricks primitive corecursion remains hopelessly primitive. The syntactic restriction for admissible corecursive definitions in Coq is more permissive in that it allows for an arbitrary number of constructors to
guard the corecursive calls, as in the following definition:
onetwos = SCons 1 (SCons 2 onetwos)

2

2015/1/23

F

Our framework achieves the same result by registering SCons as
a well-behaved operation. Intuitively, an operation is well behaved
if it needs to destruct at most one constructor of input to produce
one constructor of output. For streams, such an operation may inspect the head and the tail (but not the tail’s tail) of its arguments
before producing an SCons. Because the operation preserves productivity, it can safely surround the guarding constructor.
The rigorous definition of well-behavedness will capture this
intuition in a parametricity property that must be discharged by the
user. In exchange, the framework yields a strengthened corecursor
that incorporates the new operation.
The constructor SCons is well behaved, since it does not even
need to inspect its arguments to produce a constructor. In contrast,
the selector tail is not well behaved—it must destruct two layers of
constructors to produce one:

sup X = SCons ( (fimage head X)) (sup (fimage tail X))
Here,
fimage gives the image of a finite set under a function, and
F
X is the maximum of a finite set of naturals or 0 if X is empty.
2.2

Nested Corecursion Up-to

Although we use streams as our main example, the framework
generally supports arbitrary codatatypes with multiple curried constructors and nesting through other type constructors. To demonstrate this last feature, we introduce the type of finitely branching
Rose trees of potentially infinite depth with numeric labels:
codatatype

Tree = Node (val : Nat) (sub : List Tree)

The type Tree has a single constructor Node : Nat → List Tree →
Tree and two selectors val : Tree → Nat and sub : Tree → List Tree.
The recursive occurrence of Tree is nested in the familiar polymorphic datatype of finite lists.
We first define the pointwise sum of two trees analogously to ⊕:

tail xs = SCons (head (tail xs)) (tail (tail xs))
The presence of non-well-behaved operations in the corecursive
call context is enough to break productivity, as in the example
stallA = SCons 1 (tail stallA), which stalls immediately after producing one constructor, leaving tail stallA unspecified.
Another instructive example is the function that keeps every
other element in a stream:

t  u = Node (val t + val u)
(map (λ(t0 , u0 ). t0  u0 ) (zip (sub t) (sub u)))
Here, map is the standard map function on lists, and zip converts
two parallel lists into a list of pairs, truncating the longer list
if necessary. The criterion for primitive corecursion for nested
codatatypes requires the corecursive call to be applied through
map, which is the case for . Moreover, by virtue of being well
behaved,  can be used to define the shuffle product of trees:

everyOther xs = SCons (head xs) (everyOther (tail (tail xs)))
The function is not well behaved, despite being primitive corecursive. It also breaks productivity: stallB = SCons 1 (everyOther
stallB) stalls after producing two constructors.
Going back to our first example, we observe that the operation ⊕
is well behaved. Hence, it is allowed to participate in corecursive
call contexts when defining new functions. In this respect, the
framework is more permissive than Coq’s syntactic restriction. For
example, we can define the stream of Fibonacci numbers in either
of the following two ways:

t  u = Node (val xs × val ys)
(map (λ(t0 , u0 ). (t  u0 )  (t0  u)) (zip (sub t) (sub u)))
Again, the corecursive call takes place inside map, but this time
also in the context of . The specification of  is corecursive up-to
and well behaved.
2.3

fibA = SCons 0 (SCons 1 fibA ⊕ fibA)
fibB = SCons 0 (SCons 1 fibB) ⊕ SCons 0 fibB

Mixed Recursion–Corecursion

It is often convenient to let a corecursive function perform some
finite computation before producing a constructor. With mixed
recursion–corecursion, a finite number of unguarded recursive calls
perform this calculation before reaching a guarded corecursive call.
The intuitive criterion for accepting such definitions is that the
unguarded recursive call could be unfolded to arbitrary finite depth,
ultimately yielding a purely corecursive definition. An example is
the primes function taken from Di Gianantonio and Miculan [17]:

Well-behaved operations are allowed to appear both under the constructor guard (as in fibA) and around it (as in fibB). Notice that two
guards are necessary in the second example—one for each branch
of the ⊕ operator. Incidentally, we are not aware of any other framework that allows such definitions. Without rephrasing the specification, fibB cannot be expressed in Rutten’s format of behavioral
differential equations [46] or in Hinze’s syntactic restriction [21],
nor via Agda copatterns [5, 6].
Many useful operations are well behaved and can therefore participate in further definitions. Following Rutten, the shuffle product
⊗ of two streams is defined in terms of ⊕. Shuffle product being
itself well behaved, we can employ it to define stream exponentiation, which also turns out to be well behaved:

primes m n = if (m = 0 ∧ n > 1) ∨ gcd m n = 1
then SCons n (primes (m × n) (n + 1))
else primes m (n + 1)
When called with m = 1 and n = 2, this function computes the
stream of prime numbers. The unguarded call in the else branch
increments its second argument n until it is coprime to the first argument m (i.e., the greatest common divisor of m and n is 1). For any
positive integers m and n, the numbers m and m×n+1 are coprime,
yielding an upper bound on the number of times n is increased.
Hence, the function will take the else branch at most finitely often before taking the then branch and producing one constructor.
There is a slight complication when m = 0 and n > 1: Without the
first disjunct in the if condition, the function could stall. (This corner case was overlooked in the original example [17].)
Mixed recursion–corecursion also allows us to give a definition
of factorials without involving any auxiliary stream operations:

xs ⊗ ys = SCons (head xs × head ys)
((xs ⊗ tail ys) ⊕ (tail xs ⊗ ys))
exp xs = SCons (2 ˆ head xs) (tail xs ⊗ exp xs)
Next, we use the defined and registered operations to specify two
streams of factorials of natural numbers facA (starting at 1) and
facB (starting at 0):
facA = SCons 1 facA ⊗ SCons 1 facA
facB = exp (SCons 0 facB)
Computing the first few terms of facA manually should convince
the reader that productivity and efficiency are not synonymous.
The arguments of well-behaved operations are not restricted to
the Stream type. For example, we can define the well-behaved
supremum of a finite set of streams by primitive corecursion:

facC n a i = if i = 0 then SCons a (facC (n + 1) 1 (n + 1))
else facC n (a × i) (i − 1)
The recursion in the else branch computes the next factorial by
means of an accumulator a and a decreasing counter i. When the

3

2015/1/23

counter reaches 0, facC corecursively produces a constructor with
the accumulated value and resets the accumulator and the counter.
Unguarded calls may also occur under well-behaved operations:

distinguished by taking observations (i.e., by applying the head
and tail selectors); therefore they must be equal. In other words,
equality is the largest bisimulation.
Creativity is generally required to instantiate R with a bisimulation. However, given a goal l = r, the following canonical candidate
often works: λs t. ∃xs. s = l ∧ t = r, where xs are variables occurring free in l or r. As a rehearsal, let us prove that the primitively
corecursive operation ⊕ is commutative.

cat n = if n > 0 then cat (n − 1) ⊕ SCons 0 (cat (n + 1))
else SCons 1 (cat 1)
The call cat 1 computes
 the stream of Catalan numbers: C1 , C2 , . . . ,
1 2n
where Ci = n+1
n . This fact is far from obvious. Productivity is
not entirely obvious either, but it is guaranteed by the framework.
When mixing recursion and corecursion, it is easy to get things
wrong in the absence of solid foundations. Consider this apparently unobjectionable specification in which the corecursive call
is guarded by SCons and the unguarded call’s argument strictly decreases toward 0:

Proposition 1. xs ⊕ ys = ys ⊕ xs.
Proof. We first show that R = (λs t. ∃xs ys. s = xs ⊕ ys ∧ t = ys ⊕
xs) is a bisimulation. We fix two streams s and t for which we
assume R s t (i.e., there exist two streams xs and ys such that s =
xs ⊕ ys and t = ys ⊕ xs). Next, we must show that head s = head t
and R (tail s) (tail t). The first property can be discharged by a
simple calculation. For the second one:

nasty n = if n < 2 then SCons n (nasty (n + 1))
else inc (tail (nasty (n − 1)))

R (tail s) (tail t)
←
→ R (tail (xs ⊕ ys)) (tail (ys ⊕ xs))
←
→ R (tail xs ⊕ tail ys)) (tail ys ⊕ tail xs)
←
→ ∃xs0 ys0 . tail xs ⊕ tail ys = xs0 ⊕ ys0 ∧
tail ys ⊕ tail xs = ys0 ⊕ xs0

Here, inc = smap (λx. x + 1) and smap is the map function on
streams. A simple calculation reveals that this specification is inconsistent because the tail selector before the unguarded call destructs the freshly produced constructor from the other branch:
nasty 2 = inc (tail (nasty 1))
= inc (tail (SCons 1 (nasty 2)))
= inc (nasty 2)

The last formula can be shown to hold by selecting xs0 = tail xs and
ys0 = tail ys. Moreover, R (xs ⊕ ys) (ys ⊕ xs) holds. Therefore, the
thesis follows by structural coinduction.

This is a close cousin of the infamous f x = f x + 1 example mentioned in the introduction. The framework rejects this specification
on the grounds that the tail selector in the recursive call context is
not well behaved.
We conclude this section with a practical example from the
literature. Given the polymorphic type

If we attempt to prove the commutativity of ⊗ analogously, we
eventually encounter a formula of the form R (· · · ⊕ · · ·) (· · · ⊕ · · ·),
because ⊗ is defined in terms of ⊕. Since R mentions only ⊗ but
not ⊕, we are stuck. An ad hoc solution would be to replace the
canonical R with a bisimulation that allows for descending under ⊕.
However, this would be needed for almost every property about ⊗.
A more reusable solution is to strengthen the coinduction principle upon registration of a new well-behaved operation. The
strengthening mirrors the acquired possibility of the new operation to appear in the corecursive call context. It is technically represented by a congruence closure cl : (Stream → Stream → Bool) →
Stream → Stream → Bool. The coinduction up-to principle is almost identical to structural coinduction, except that the corecursive
application of R is replaced by cl R:

LList(A) =
LNil | LCons (head : A) (tail : LList(A))

codatatype

of lazy lists, the task is to define the function lfilter : (A → Bool) →
LList(A) → LList(A) that filters out all elements failing to satisfy
the given predicate. Thanks to the support for mixed recursion–
corecursion, the framework transforms what was for Lochbihler
and Hölzl [36] a research problem into a routine exercise:
lfilter P xs = if ∀x ∈ xs. ¬ P xs
then LNil
else if P (head xs)
then LCons (head xs) (lfilter P (tail xs))
else lfilter P (tail xs)

∀s t. R s t −→ head s = head t ∧ cl R (tail s) (tail t)
l=r
The principle evolves with every newly registered well-behaved
operation in the sense that our framework refines the definition of
the congruence closure cl. (Strictly speaking, a fresh symbol cl0 is
introduced each time.) For example, after registering SCons and ⊕,
cl R is the least reflexive, symmetric, transitive relation containing R
and satisfying the rules
Rlr

The first self-call is corecursive and guarded by LCons, whereas
the second self-call is terminating, because the number of “false”
elements until reaching the next “true” element (whose existence is
guaranteed by the first if condition) decreases by one.
2.4

x = y cl R xs ys
cl R (SCons x xs) (SCons y ys)

Coinduction Up-to

Once a corecursive specification has been accepted as productive,
we normally want to reason about it. In proof assistants, codatatypes are accompanied by a notion of structural coinduction that
matches primitively corecursive functions. For nonprimitive specifications, our framework provides the more advanced proof principle of coinduction up to congruence—or simply coinduction up-to.
The structural coinduction principle for streams is as follows:

cl R xs ys cl R xs0 ys0
cl R (xs ⊕ xs0 ) (ys ⊕ ys0 )

After defining and registering ⊗, the relation cl R is extended to
also satisfy
cl R xs ys cl R xs0 ys0
cl R (xs ⊗ xs0 ) (ys ⊗ ys0 )
Let us apply the strengthened coinduction principle to prove the
distributivity of stream exponentiation over pointwise addition:
Proposition 2. exp (xs ⊕ ys) = exp xs ⊗ exp ys.

∀s t. R s t −→ head s = head t ∧ R (tail s) (tail t)
l=r
Coinduction allows us to prove an equality on streams by providing
a relation R that relates the left-hand side with the right-hand
side (first premise) and that constitutes a bisimulation (second
premise). Streams that are related by a bisimulation cannot be
Rlr

Proof. We first show that R = (λs t. ∃xs ys. s = exp (xs ⊕ ys) ∧ t =
exp xs ⊗ exp ys) is a bisimulation. We fix two streams s and t for
which we assume R s t (i.e., there exist two streams xs and ys such
that s = exp (xs ⊕ ys) and t = exp xs ⊗ exp ys). Next, we show that
head s = head t and cl R (tail s) (tail t):

4

2015/1/23

• a functorial action Fmap : ∏A,B∈Setn ∏ni=1 (Ai → Bi ) → F A →

head s = head (exp (xs ⊕ ys)) = 2 ˆ head (xs ⊕ ys)
= 2 ˆ (head xs + head ys) = 2 ˆ head xs × 2 ˆ head ys
= head (exp xs) × head (exp ys)
= head (exp xs ⊗ exp ys) = head t

F B, i.e., a polymorphic function of the indicated type that
commutes with identity idA : A → A and composition;

• a relator Frel : ∏A,B∈Setn ∏ni=1 (Ai → Bi → Bool) → F A →

F B → Bool, i.e., a polymorphic function of the indicated type
which commutes with binary-relation identity and composition.

cl R (tail s) (tail t)
←
→ cl R (tail (exp (xs ⊕ ys))) (tail (exp xs ⊗ exp ys))
←
→ cl R ((tail xs ⊕ tail ys) ⊗ exp (xs ⊕ ys))
(exp xs ⊗ (tail ys ⊗ exp ys) ⊕ (tail xs ⊗ exp xs) ⊗ exp ys)
∗
←
→ cl R ((tail xs ⊗ exp (xs ⊕ ys) ⊕ tail ys ⊗ exp (xs ⊕ ys))
⊕ (tail xs ⊗ (exp xs ⊗ exp ys) ⊕ tail ys ⊗ (exp xs ⊗ exp ys)
←− cl R (tail xs ⊗ exp (xs ⊕ ys)) (tail xs ⊗ (exp xs ⊗ exp ys)) ∧
⊗ cl R (tail ys ⊗ exp (xs ⊕ ys)) (tail ys ⊗ (exp xs ⊗ exp ys))
←− cl R (tail xs) (tail xs) ∧ cl R (tail ys) (tail ys) ∧
cl R (exp (xs ⊕ ys)) (exp xs ⊗ exp ys)
←− R (exp (xs ⊕ ys)) (exp xs ⊗ exp ys)

Following standard notation from category theory, we write F instead of Fmap. Given binary relations Ri : Ai → Bi → Bool for
1 ≤ i ≤ n, we think of Frel R : F A → F B → Bool as the natural
lifting of R along F; for example, if F is List (and hence n = 1),
Frel lifts a relation on elements to the componentwise relation on
lists (also requiring equal length). It is well known that the positive
type constructors defined by standard means (basic types, composition, least or greatest fixpoints) have canonical functorial and relator structure. This is crucial for the foundational construction of
user-specified (co)datatypes in Isabelle/HOL [49].
But even nonpositive type constructors G : Setn → Set exhibit a relator-like structure Grel : ∏A,B∈Setn (A → B) → (G A →
G B → Bool) (which need not commute with relation composition, though). For example, if G : Set2 → Set is the functionspace constructor G (A1 , A2 ) = A1 → A2 and f ∈ G (A1 , A2 ),
g ∈ G (B1 , B2 ), R1 : A1 → B1 → Bool, and R2 : A2 → B2 → Bool,
then Grel R1 R2 f g is defined as ∀a1 ∈ A1 . ∀b1 ∈ B1 . R1 a1 b1 −→
R2 ( f a1 ) (g b1 ). A polymorphic function c : ∏A∈Setn G A, c
is called parametric [41, 52] if ∀A, B ∈ Setn . ∀R : A → B →
Bool. Grel R cA cB . The maintenance of relator-like structures is
very helpful for automating theorem transfer along isomorphisms
and quotients [24]. Here we explore an additional benefit of maintaining functorial and relator structure for type constructors: the
possibility to extend the corecursor in reaction to user input.
In this section, we assume that all the considered type constructors are both functors and relators, that they include basic functors such as identity, constant, sum, and product, and that they are
closed under least fixpoints (initial algebras) and greatest fixpoints
(final coalgebras). Examples of such classes of type constructors
include the datafunctors [20], the containers [1], and the bounded
natural functors [49].
We focus on the case of a unary codatatype-generating functor
F : Set → Set. The codatatype of interest will be its greatest fixpoint
(or final coalgebra) J = gfp F. This generic situation already covers
the vast majority of interesting codatatypes, since F can represent
arbitrarily complex nesting. For example, if F = (λA. Nat×List A),
then J corresponds to the Tree codatatype presented in Section 2.2.
The extension to mutually defined codatatypes is straightforward
but tedious. Our examples will take J to be the Stream type from
Section 2, with F = (λA. Nat × A).
Given a set A, it will be useful to think of the elements x ∈ F A as
consisting of a shape together with content that fills the shape with
elements of A. If F A = Nat × A, the shape of x = (n, a) is (n, _)
and the content is a; if F A = List A, the shape of x = [x1 , . . . , xn ]
is the n-slot container [_, . . . , _] and the content consists of the xi ’s.
According to this view, for each f : A → B, the functorial
action associated with F sends any x into an element F f x of the
same shape as x but with each content item a replaced by f a.
Technically, this view can be supported by custom notions such
as containers [1] or, more simply, via a parametric function of type
∏A∈Set F A → Set A that collects the content elements [49].

The step marked with ∗ appeals to associativity and commutativity
of ⊕ and ⊗ as well as distributivity of ⊗ over ⊕. These properties
are likewise proved by coinduction up-to. The implications marked
with ⊕ and ⊗ are justified by the respective congruence rules. The
last implication uses reflexivity and expands R to its closure cl R.
Finally, it is easy to see that R (exp (xs ⊕ ys)) (exp xs ⊗ exp ys)
holds. Therefore, the thesis follows by coinduction up-to.
The formalization accompanying this paper [13] also contains
proofs of facA = facC 1 1 1 = smap fac (natsFrom 1), facB =
SCons 1 facA, and fibA = fibB, where fac is the factorial on Nat.
Nested corecursion up-to is also reflected with a suitable
strengthened coinduction rule. For Tree, this strengthening takes
place under the rel operator on list, similarly to the corecursive
calls occurring nested in the map function:
∀s t. R s t −→ val s = val t ∧ rel (cl R) (sub s) (sub t)
l=r
The rel R operator lifts the binary predicate R : A → B → Bool to
a predicate List A → List B → Bool. More precisely, rel R xs ys
holds if and only if xs and ys have the same length and parallel
elements of xs and ys are related by R. This nested coinduction
rule is convenient provided there is some infrastructure to descend
under rel (as is the case in Isabelle/HOL). The formalization [13]
establishes several arithmetic properties of  and .
Rlr

3.

Extensible Corecursors

We now describe the definitional and proof mechanisms that substantiate flexible corecursive definitions in the style of Section 2.
They are based on the modular maintenance of infrastructure for
the corecursor associated with a codatatype, with the possibility of
open-ended incremental improvement. We present the approach for
an arbitrary codatatype given as the greatest fixpoint of an arbitrary
(bounded) functor. The approach is quite general and does not rely
on any particular grammar for specifying codatatypes.
Extensibility is an integral feature of the framework. In principle, an implementation could redo the constructions from scratch
each time a well-behaved operation is registered, but it would
give rise to a quadratic number of definitions, slowing down the
proof assistant. The incremental approach is also more flexible and
future-proof, allowing mixed fixpoints and composition with other
(co)recursors, including some that do not exist yet.
3.1

Functors and Relators
3.2

Functional programming languages and proof assistants necessarily maintain a database of the user-defined types or, more generally,
type constructors, which can be thought as functions F : Setn → Set
operating on sets (or perhaps on ordered sets). It is often useful to
maintain more structure along with these type constructors:

Primitive Corecursion

The codatatype that defines J also introduces the constructor and
destructor bijections ctor : F J → J and dtor : J → F J and the primitive corecursor corecPrim : ∏A∈Set (A → F A) → A → J characterized by the equation corecPrim s a = ctor (F (corecPrim s) (s a)).

5

2015/1/23

In elements x ∈ F A, the occurrences of content items a ∈ A in the
shape of x captures the positioning of the corecursive calls.
Example 3. Modulo currying, the pointwise sum of streams ⊕ is
definable as corecPrim s, by taking s : Stream2 → Nat × Stream2
to be λ(xs, ys). (head xs + head ys, (tail xs, tail ys)).

/J
O

Λ◦Σ hid,dtori◦ιi

ctor



F (Σ∗ J)

In Example 3 and elsewhere, we lighten notation by identify
the curried and uncurried forms of functions, counting on implicit
coercions between the two.
3.3

fi

Ki J

F eval

/ FJ

Figure 1: The well-behavedness condition

The Corecursion State

Given any functor Σ : Set → Set, we define its free-monad functor
Σ∗ by Σ∗ A = lfp (λB. A + Σ B). We write leaf : A → Σ∗ A and
op : Σ (Σ∗ A) → Σ∗ A for the left and right injections into Σ∗ A.
The functions leaf and op are in fact polymorphic; for example,
leaf has type ∏A∈Set A → Σ∗ A. We often omit the set parameters
of polymorphic functions if they can be inferred from the context,
writing leaf and op instead of leaf A and opA .
At any given moment, we maintain the following data associated with J, which we call a corecursion state:

But what guarantees that the fi ’s are indeed safe as contexts for
corecursive calls? In particular, how can the framework exclude tail
while allowing SCons, ⊕, and ⊗? This is where the parametricity
and well-behavedness conditions on the state enter the picture.
We start with well-behavedness. Assume x ∈ Ki , which is unambiguously represented in Σ as ιi x. Let j1 , . . . , jm ∈ J be the content
items of ιi x (placed in various slots in the shape of x). To evaluate fi
on x, we first corecursively destruct the jl ’s while also keeping the
originals, thus replacing each jl with ( jl , dtor jl ). Then we apply
the transformation Λ to obtain an element of F (Σ∗ J), which has
an F-shape at the top (the first produced observable data) and for
each slot in this shape an element of Σ∗ J, i.e., a formal-expression
tree having leaves in J and built using operation symbols from the
signature (the corecursive continuation):

• a finite number of functors K1 , . . . , Kn : Set → Set and, for each

Ki , a function fi : Ki J → J;
• a polymorphic function Λ : ∏A∈Set Σ (A × F A) → F (Σ∗ A).

We call the fi ’s the well-behaved operations and define their collective signature functor Σ as λA. K1 A+· · ·+Kn A, where ιi : Ki → Σ
is the standard embedding of Ki into Σ. We call Λ the corecursor
seed. The corecursion state is subject to the following conditions:

ι

i
Ki J −→
ΣJ

Σ hid,dtori

−→

Σ (J × F J) −→ F (Σ∗ J)
Λ

In summary, Λ is a schematic representation of the mutually corecursive behavior of the well-behaved operations up to the production of the first observable data. This intuition is made formal in the
well-behavedness condition, which states that the diagram in Figure 1 commutes for each fi . (We could replace the right upward arrow labeled by ctor with a downward arrow labeled by dtor without
changing the diagram’s meaning. However, we consistently prefer
the constructor view in our exposition.)
In the above explanations, we saw that it suffices to peel off one
layer of the arguments ji (by applying dtor) for a well-behaved
operation fi to produce, via Λ, one layer of the result and to
delegate the rest of the computation to a context consisting of a
combination of well-behaved operations (an element of Σ∗ J). But
how to formally express that exploring one layer is enough, i.e.,
that applying Λ : J × F J → F (Σ∗ J) to ( ji , dtor ji ) does not result
in a deeper exploration? An elegant way of capturing this is to
require that Λ, which is a polymorphic function, operates without
analyzing J, i.e., that it operates in the same way on A × F A →
F (Σ∗ A) for any set A. This requirement is precisely parametricity.
Strictly speaking, the well-behaved operations f are a redundant
piece of data in the state (K, f , Λ), since, assuming Λ parametric,
we can prove that there exists a unique tuple f that satisfies the
well-behavedness condition. In other words, the operations f could
be derived on a per-need basis.

Parametricity: Λ is parametric.
Well-behavedness: Each fi satisfies the characteristic equation
fi x = ctor (F eval (Λ (Σ hid, dtori (ιi x))))
The convolution operator h_, _i builds a function h f, gi : B → C × D
from two functions f : B → C and g : B → D, and eval : Σ∗ J → J
is the canonical evaluation function defined recursively (using the
primitive recursor associated with Σ∗ ):
eval (leaf j) = j
eval (op z) = case z of ιi t ⇒ fi (Ki eval t)
(Note that, on the recursive call on the right eval, is applied to t via
“lifting” it through the functor Ki .) Functions having the type of
Λ and additionally assumed parametric (or, equivalently, assumed
to be natural transformations) are known in category theory as
“abstract GSOS rules.” They were introduced by Turi and Plotkin
[50] and further studied by Bartels [8], Jacobs [26], Hinze and
James [22], Milius et al. [38], and others.
Thus, a corecursion state is a triple (K, f , Λ). As we will see
in Section 3.6, the state evolves as users define and register new
functions. The fi ’s are the operations that have been registered as
safe for participating in the context of corecursion calls. Since fi
has type Ki J → J, we think of Ki as encoding the arity of fi . Then
Σ, the sum of the Ki ’s, represents the signature consisting of all the
fi ’s. Thus, for each A, Σ∗ A represents the set of formal expressions
over Σ and A, i.e., the trees built starting from the “variables” in
A as leaves by applying operations symbols corresponding to the
fi ’s. Finally, eval evaluates in J the formal expressions of Σ∗ J by
applying the functions fi recursively.
If the functors Ki are restricted to be finite monomials λA. Aki ,
the functor Σ can be seen as a standard algebraic signature and
(Σ∗ A, op) as the standard term algebra for this signature, over the
variables A. However, we allow Ki to be more exotic; for example,
Ki A can be ANat (representing an infinitary operation) or one of
List A and FinSet A (representing an operation taking a varying
finite number of ordered or unordered arguments).

Example 4. Let J = Stream and assume that SCons : Nat ×
Stream → Stream and ⊕: Stream2 → Stream are the only wellbehaved operations registered so far. Then K1 = (λB. Nat × B),
f1 = SCons, K2 = (λB. B2 ), and f2 = ⊕. Moreover, Σ∗ = lfp (λB.
A + (Nat × B + B2 )) consists of formal-expression trees with
leaves in A and built using arity-correct applications of operation
symbols corresponding to SCons and ⊕, denoted by SCons and
⊕ . Given n ∈ Nat and a, b ∈ A, an example of such a tree is
leaf a ⊕ SCons (n, leaf a ⊕ leaf b). If additionally A = J, then
eval applied to the above tree is a ⊕ SCons n (a ⊕ b).
But what is Λ? As we show below, we need not worry about
the global definition of Λ, since both Σ and Λ will be updated
incrementally when registering new operations as well behaved.

6

2015/1/23

Nonetheless, a global definition of Λ for SCons and ⊕ follows:

operations were registered):

Λ z = case z of
ι1 (n, (a, (m, a0 ))
⇒ (n, SCons (m, leaf a0 ))
ι2 ((a, (m, a0 )), (b, (n, b0 ))) ⇒ (m + n, leaf a0 ⊕ leaf b0 )

⊕, everyOther:
corecFlex, corecTop, corecPrim
onetwos, fibA, ⊗, exp, sup: corecFlex, corecTop
fibB, facA, facB:
corecFlex

Informally, SCons and ⊕ exhibit the following behaviors:

With the usual identification of Unit → J and J, we can define fibA
and facA as follows:

• to evaluate SCons on a number n and an item a with (head a,

tail a) = (m, a0 ), produce n and evaluate SCons on m and a0 ,
i.e., output SCons n (SCons m a0 ) = SCons n a;
• to evaluate ⊕ on a, b with (head a, tail a) = (m, a0 ) and
(head b, tail b) = (n, b0 ), produce m + n and evaluate ⊕ on
a0 and b0 , i.e., output SCons (m + n) (a0 ⊕ b0 ).
3.4

fibA = corecTop (λu : Unit. (0, SCons (1, leaf u) ⊕ (leaf u)))
facA = corecFlex (λu : Unit. leaf (1, leaf u) ⊗ leaf (1, leaf u))
Let us look at fibA closely, comparing its specification fibA =
SCons 0 (SCons 1 fibA ⊕ fibA) with its definition in terms of
corecTop. The outer SCons guard (with 0 as first argument) corresponds to the outer pair (0, _). The inner SCons and ⊕ are interpreted as well-behaved operations and represented by the symbols
SCons and ⊕ (cf. Example 4). Finally, the corecursive calls of
fibA are captured by leaf u.
The desired specification can be obtained from the corecTop
form by the characteristic equation of corecTop (for A = Unit) and
the properties of eval as follows, where we simply write s, fibA,
and leaf instead of their applications to the unique element () of
Unit, namely s (), fibA (), and leaf ():

Corecursion Up-to

A corecursion state (K, f , Λ) for an F-defined codatatype J consists
of a collection of operations on J, fi : Ki J → J, that satisfy the
well-behavedness properties expressed in terms of a parametric
function Λ. We are now ready to harvest the crop of this setting: a
corecursion principle for defining functions having J as codomain.
The principle will be represented by two corecursors, corecTop
and corecFlex. Although subsumed by the latter, the former is interesting in its own right and will give us the opportunity to illustrate
some fine points. Below we list the types of these corecursors along
with that of the primitive corecursor for comparison:

fibA
=

{by the commutativity of Figure 2b
with fibA = corecTop s}
ctor (F (eval ◦ Σ∗ fibA) s)
=
{by the definitions of F and s}
SCons 0 ((eval ◦ Σ∗ fibA) ( SCons (1, leaf) ⊕ (leaf)))
=
{by the definition of Σ∗ }
SCons 0 (eval ( SCons (1, leaf fibA) ⊕ (leaf fibA))
=
{by the definition of eval}
SCons 0 (SCons 1 fibA ⊕ fibA)

Primitive corecursor:
corecPrim : ∏A∈Set (A → F A) → A → J
Top-guarded corecursor up-to:
corecTop : ∏A∈Set (A → F (Σ∗ A)) → A → J
Flexibly guarded corecursor up-to:
corecFlex : ∏A∈Set (A → Σ∗ (F (Σ∗ A))) → A → J
Figure 2 presents the diagrams whose commutativity properties
give the characteristic equations of these corecursors.
Each corecursor implements a contract of the following form:
If, for each a ∈ A, one provides the intended corecursive behavior
of g a represented as s a, where s is a function from A, one obtains
the function g : A → J (as the corresponding corecursor applied to
s) satisfying a suitable fixpoint equation matching this behavior.
The codomain of s is the key to understanding the expressiveness of each corecursor. The intended corecursive calls are represented by A, and the call context is represented by the surrounding
combination of functors (involving F, Σ∗ , or both):

The elimination of the corecTop infrastructure relies on simplification rules for the involved operators and can be fully automatized.
Parametricity and well-behavedness are crucial for proving that
the corecursors actually exist:
Theorem 6. There exist the polymorphic functions corecTop and
corecFlex making the diagrams in Figures 2b and 2c commute.
Moreover, for each s of appropriate type, corecTop s or corecFlex s
is the unique function making its diagram commute.
Theorem 6 is a known result from the category theory literature: The corecTop s version follows from the results in Bartels’s
thesis [9], whereas the corecFlex s version was very recently (and
independently) proved by Milius et al. [38, Theorem 2.16].

• for corecPrim, the allowed call contexts consist of a single

constructor guard (represented by F);
• for corecTop, they consist of a constructor guard (represented

by F) followed by any combination of well-behaved operations
fi (represented by Σ∗ );

3.5

Initializing the Corecursion State

The simplest relaxation of primitive corecursion is the allowance
of multiple constructors in the call context, in the style of Coq,
as in the definition of onetwos (Section 2.1). Since this idea is
independent of the choice of codatatype J, we realize it when
bootstrapping the corecursion state.
More precisely, upon defining a codatatype J, we take the following initial corecursion state initState = (K, f , Λ):

• for corecFlex, they consist of any combination of well-behaved

operations satisfying the condition that on every path leading
to a corecursive call there exists at least one constructor guard
(represented by Σ∗ (F (Σ∗ _))).
We can see the computation of g a by following the diagrams in
Figure 2 counterclockwise from their left-top corners. The application s a first builds the call context syntactically. Then g is applied
corecursively on the leaves. Finally, the call context is evaluated:
for corecPrim, it consist only of the guard (ctor); for corecTop, it
involves the evaluation of the well-behaved operators (which may
also include several occurrences of the guard) and ends with the
evaluation of the top guard; for corecFlex, the evaluation of the
guard is interspersed with that of the other well-behaved operations.

• K is a singleton consisting of (a copy of) F;
• f is a singleton consisting of ctor;
• Λ : ∏A∈Set F (A×F A) → F (F∗ A) is defined as F (op ◦ F leaf ◦

snd), where snd is the second product projection.
Recall that the seed Λ is designed to schematically represent the
corecursive behavior of the registered operations by describing
how they produce one layer of observable data. The definition in

Example 5. For each example from Section 2.1, we give the corecursors that can handle it (assuming the necessary well-behaved

7

2015/1/23

A
s

s

/J
O

corecPrim s

FA

s

F (Σ∗ A)

/J
O

corecFlex s

A

ctor



eval



Σ∗ (F (Σ∗ A))

;F J

Σ∗O J

F eval

ctor



/J
O

corecTop s

A

F (Σ∗ (corecTop s))
F (corecPrim s)

/ FJ

Σ∗ (F (Σ∗ (corecFlex s)))

%

F (Σ∗ J)

(a) Primitive corecursion

Σ∗ ctor

(

Σ∗ (F (Σ∗ J))

(b) Top-guarded corecursion up-to

Σ∗ (F eval)

/ Σ∗ (F J)

(c) Flexibly guarded corecursion up-to

Figure 2: The corecursors

F (A × F A)

/ F (F∗ A)
O

Λ

K hid,dtori


F (F A)

ctor

(

K (J × F J)

s

8 FJ

ρ

F op

F snd

/J
O

g = corecTop s

KJ



F (F leaf)

/ F (F (F∗ A))

v

F (Σ∗ (K J))

(a) Definition of Λ for the initial state

F (Σ∗ g)

F eval

/ F (Σ∗ J)

(b) A new well-behaved operation g

Figure 3: Definitions of Λ and g

Figure 3a depicts this for ctor and instantiates to the schematic
behavior of SCons presented at the end of Example 4.

Theorem 8. If (K, f , Λ) is a well-formed corecursion state, so is
nextStateg (K, f , Λ).

Theorem 7. initState is a well-formed corecursion state—i.e., it
satisfies parametricity and well-behavedness.

In summary, we have the following scenario triggering the
state’s advancement:

3.6

1. One defines a new operation g = corecTop s.

Advancing the Corecursion State

2. One shows that s factors through a parametric function ρ and
K hid, dtori (as in Figure 3b); in other words, one shows that g’s
corecursive behavior s decomposes into a one-step destruction
of the arguments and a parametric transformation (which is
independent of J).

The role of a corecursion state (K, f , Λ) for J is to provide infrastructure for flexible corecursive definitions of functions g between
arbitrary sets A and J. If nothing else is known about A, this is
the end of the story. However, assume that J is a component of A,
in that A is constructed from J (possibly along with other components). For example, A could be List J, or J × (Nat → List J). We
capture this abstractly by assuming A = K J for some functor K.
In this case, we have a fruitful situation of which we can profit
for improving the corecursion state, and hence improving the flexibility of future corecursive definitions. Under some uniformity assumptions, g itself can be registered as well behaved.
More precisely, assume that g : K J → J is defined by g =
corecTop s and that s can be proved to be uniform in the following
sense: There exists a parametric function ρ : ∏A∈Set K (A × F A) →
F (Σ∗ (K A)) such that s = ρ ◦ Khid, dtori (Figure 3b). Then we
can integrate g as a well-defined operation as follows. We define
nextStateg (K, f , Λ), the “next” corecursion state triggered by g,
as (K0 , f 0 , Λ0 ), where

3. The corecursion state is updated by nextStateg .
Example 9. The operations onetwos, ⊕, ⊗, and exp from Section 2.1 are covered by this scenario. For example, assume that
SCons and ⊕ are registered as well behaved at the time of defining ⊗ (cf. Example 4). Then K = (λA. A2 ) and ⊗ = corecTop s,
where
s = (λ(xs, ys). (head xs × head ys,
leaf (xs, tail ys) ⊕ leaf (tail xs, ys)))
The function s decomposes into ρ ◦ K hid, hhead, tailii, where
ρ : ∏A∈Set (A × (Nat × A))2 → Nat × Σ∗ (A2 )
is defined by ρ ((a, (m, a0 )), (b, (n, b0 ))) = (m×n, (a, b0 ) ⊕ (a0 , b)),
which is clearly parametric. The act of determining ρ from s and
K hid, hhead, tailii is syntax-directed.

• K0 = (K1 , . . . , Kn , K) (similarly to Σ versus K, we write Σ0

for the signature functor of K0 ; note that we essentially have
Σ0 = Σ + K);

• f 0 = ( f1 , . . . , fn , g);

3.7

• Λ0 : ∏A∈Set Σ0 (A×F A) → F (Σ0 ∗ A) is defined as [Λ ◦ F embL,

Coinduction Up-to

In a proof assistant, specification mechanisms are not very useful
unless they are complemented by suitable reasoning infrastructure.
The natural counterpart of corecursion up-to is coinduction up-to.
In our incremental framework, the expressiveness of coinduction
up-to grows together with that of corecursion up-to.

ρ ◦ F embR] where [_, _] is the case operator on sums, which
builds a function [u, v] : B +C → D from two functions u : B →
D and v : C → D, and embL : Σ∗ A → Σ0 ∗ A, embR : Σ∗ (K A) →
Σ0 ∗ A are the natural embeddings into Σ0 ∗ A.

8

2015/1/23

Σ∗ [leaf, flat], where flat : ∏A∈Set Σ∗ (Σ∗ A) → A is the standard join operation of the Σ∗ -monad.

We start with structural coinduction [45], allowing to prove two
elements of J equal by exhibiting an F-bisimulation, i.e., a binary
relation R on J such that whenever two elements j1 and j2 are
related, their dtor-unfoldings are componentwise related by R.

• eval_(F _+_) evaluates all the formal operations of Σ∗ :

eval_(F _+_) = eval ◦ Σ∗ ([ctor ◦ F eval, eval])

∀ j1 j2 ∈ J. R j1 j2 −→ Frel R (dtor j1 ) (dtor j2 )
j1 = j2
Recall that our type constructors are not only functors but also
relators. The notion of “componentwise relationship” refers to F’s
relator structure Frel.
Upon integrating a new operation g (Section 3.6), the coinduction rule is made more flexible by allowing the dtor-unfoldings to
be componentwise related not only by R but more generally by a
closure of R that takes g into account.
For a corecursion state (K, f , Λ) and a relation R : J → J →
Bool, we define cl f R, the f -congruence closure of R, as the smallest equivalence relation that includes R and is compatible with each
fi : Ki J → J:
R j 1 j2

Theorem 11. If there exists (a unique) g : A → Σ∗ (F (Σ∗ A)) such
that the diagram in Figure 4a commutes, there exists (a unique)
f : A → J such that the diagram in Figure 4b commutes, namely,
corecFlex g.
The theorem certifies the following procedure for making sense
of a mixed fixpoint definition of a function f :
1. Separate the guarded and the unguarded calls (as shown in the
codomain Σ∗ (F (Σ∗ A) + Σ∗ A) of s).
2. Prove that the unguarded calls eventually terminate or lead to
guarded calls (as witnessed by g).
3. Pass the unfolded guarded calls to the corecursor—i.e., take
f = corecFlex g.

∀z1 , z2 ∈ Ki J. Kreli R z1 z2 −→ cl f R ( fi z1 ) ( fi z2 )

Example 12. The above procedure can be applied to define facC,
primes : Nat → Nat → Stream, and cat : Nat → Stream, while
avoiding the unsound nasty (Section 2.3). A simple analysis reveals
that the first self-call to primes is guarded while the second is not.
We define g : Nat × Nat → Σ∗ (Nat × Σ∗ (Nat × Nat)) by

where Kreli is the relator associated with Ki .
The next theorem supplies the reasoning counterpart of the
definition principle stated in Theorem 6. It can be inferred from
recent, more abstract results [43].
Theorem 10. The following coinduction rule up to f holds in the
corecursion state (K, f , Λ):
R j1 j2

g (m, n) = if (m = 0 ∧ n > 1) ∨ gcd m n = 1
then leaf (n, leaf (m × n, n + 1))
else g (m, n + 1)

∀ j1 j2 ∈ J. R j1 j2 −→ Frel (cl f R) (dtor j1 ) (dtor j2 )
j1 = j2

In essence, g behaves like (the intended) f except that the guarded
calls are left symbolic, whereas the unguarded calls are interpreted
as actual calls to g. One can show that g is well defined by a
standard termination argument. This characteristic equation of g is
the commutativity of the diagram determined by s as in Figure 4a,
where s : Nat × Nat → Σ∗ (Nat × Σ∗ (Nat × Nat) + Σ∗ (Nat ×
Nat)) is defined as follows (with Inl and Inr being the left and right
sum embeddings):

Coinduction up to f is the ideal abstraction for proving equalities involving functions defined by corecursion up to f : For example, a proof of commutativity for ⊗ naturally relies on contexts involving ⊕, because ⊗’s corecursive behavior (i.e., ⊗’s dtorunfolding) depends on ⊕.

4.

Mixed Fixpoints

s (m, n) = if (m = 0 ∧ n > 1) ∨ gcd m n = 1
then leaf (Inl (leaf (n, leaf (m × n, n + 1))))
else leaf (Inr (leaf (m, n + 1)))

When we write fixpoint equations to define a function f , we often
want to distinguish corecursive calls from calls that are sound
for other reasons—for example, if they terminate. We model this
situation abstractly by a function s : A → Σ∗ (F (Σ∗ A) + Σ∗ A). As
usual for each a, the shape of s a represents the calling context for
f a, with the occurrences of the content items a0 in s a representing
calls to f a0 . The new twist is that we now distinguish guarded calls
(captured by the left-hand side of +) from possibly unguarded ones
(the right-hand side of +).
We want to define a function f with the behavior indicated by
s, i.e., making the diagram in Figure 4b commute. In the figure, +
denotes the map function u + v : B + C → D + E built from two
functions u : B → D and v : C → E. In the absence of pervasive
guards, we cannot employ the corecursors directly to define f .
However, if we can show that the noncorecursive calls eventually
lead to a corecursive call, we will be able to employ corecFlex.
This precondition can be expressed in terms of a fixpoint equation.
According to Figure 4a, the call to g (shown on the base arrow)
happens only on the right-hand side of +, meaning that the intended
corecursive calls are ignored when “computing” the fixpoint g. Our
goal is to show that the remaining calls behave properly.
The functions reduce and eval that complete the diagrams of
Figure 4 are the expected ones:

Setting primes = corecFlex g yields the desired characteristic equation for primes after simplification (cf. Example 4).
The primes example has all unguarded calls in tail form, which
makes the associated function g tail-recursive. This need not be the
case, as shown by the cat example, whose unguarded calls occur
under the well-behaved operation ⊕. However, we do require that
the unguarded calls occur in contexts formed by well-behaved operations alone. After unfolding all the unguarded calls, the resulting
context that is to be handled corecursively must be well behaved—
this precludes unsound definitions like nasty.

5.

Formalization and Implementation

We formalized in Isabelle/HOL the metatheory of Sections 3 and 4.
Essentially, this means that the results have been proved in higherorder logic with Infinity, Choice, and a mechanism for defining
types by exhibiting non-empty subsets of existing types. The logic
is comparable to Zermelo set theory with Choice (ZC) but weaker
than ZFC. The development would work for any class of functors
that are relators (or closed under weak pullbacks), contain basic
functors (identity, (co)products, etc.) and are closed under intersection, composition, and have initial algebras and final coalgebra that
can be represented in higher-order logic. However, our Isabelle development focuses on a specific class [49].

• The elements of Σ∗ (F (Σ∗ A)) are formal-expression trees

guarded on every path to the leaves, and so are the elements
Σ∗ (F (Σ∗ A) + Σ∗ (Σ∗ (F (Σ∗ A)))), but with a more restricted
shape; reduce embeds the latter in the former: reduce = flat ◦

9

2015/1/23

/ Σ∗ (F (Σ∗ A))
O

g

A
s

A



Σ∗ (id+Σ∗ g)

eval_(F _+_)

s

reduce

Σ∗ (F (Σ∗ A) + Σ∗ A)

/J
O

f = corecFlex g



/ Σ∗ (F (Σ∗ A) + Σ∗ (Σ∗ (F (Σ∗ A)))))

Σ∗ (F (Σ∗ A) + Σ∗ A)

(a) Assumption

Σ∗ (F (Σ∗ f )+Σ∗ f )

/ Σ∗ (F (Σ∗ J) + Σ∗ J)

(b) Conclusion

Figure 4: Mixed fixpoint
4. Extract a polymorphic function ρ from the specification of f.

The formalization consists of two parts: The base derives a corecursor up-to from a primitive corecursor; the step starts with a corecursor up-to and integrates an additional well-behaved operation.
The base part starts by axiomatizing a functor F and defines a
codatatype with nesting through F: codatatype J = ctor (F J).
(In general, J could depend on type variables, but this is an orthogonal concern that would only clutter the formalization.) Then the
formalization defines the free algebra over F and the basic corecursor seed Λ for initializing the state with ctor as well behaved (Section 3.5). It also needs to lift Λ to the free algebra, a technicality that
was omitted in the presentation. Then it defines eval and other necessary structure (Section 3.3). Finally, it introduces corecTop and
corecFlex (Section 3.4) and derives the corresponding coinduction
principle (Section 3.7).
From a high-level point of view, the step part has a somewhat
similar structure to the base. It axiomatizes a domain functor K
and a parametric function ρ associated with the new well-behaved
operation g to integrate. Then it extends the signature to include
K, defines the extended corecursor seed Λ0 , and lifts Λ0 to the
free algebra. Next, it defines the parameterized evalg and other
infrastructure (Section 3.6). Finally, it introduces corecTop and
corecFlex for the new state and derives the coinduction principle.
The process of instantiating the metatheory to particular userspecified codatatypes is automated by a prototype tool: the user
points to a particular codatatype (typically defined using Isabelle’s
existing (co)datatype specification language [12]), and then the tool
takes over and instantiates the generic corecursor to the indicated
type, provinding the concrete corecursion and mixed recursioncorecursion theorems. The stream and tree examples presented in
Section 2 have all been obtained with this tool. As a larger case
study, we formalized all the examples from the extended version
of Hinze and James’s study [22]. The parametricity proof obligations were discharged by Isabelle’s parametricity prover [24]. The
mixed recursion–corecursion definitions were done using Isabelle’s
facility for defining terminating recursive functions [29].
Unlike Isabelle’s primitive (co)recursion mechanism [12], our
tool currently lacks syntactic sugar support, so it still requires
some boilerplate from the user, namely the explic invocation of the
corecursor and the parametricity prover: these are just a few extra
lines of script per definition, and therefore the tool is also usable
in the current form. Following the design of its primitive ancestor,
its envisioned fully user-friendly extension will replace the explicit
invocation of the corecursor with a corec command, allowing
users to specify a function f corecursively and then performing the
following steps (cf. Example 5):

5. Automatically prove ρ parametric or pass the proof obligation
to the user.
6. Derive the new strengthened corecursor and its new coinduction
principle.
The corec command will be complemented by an additional command, tentatively called well_behaved_for_corec, for registering
arbitrary operations f (not necessarily defined using corec) as well
behaved. The command will ask the user to provide a corecursive
specification of f as a lemma of the form f x = Cons . . . and then
perform steps 4 to 6. The corec command will become stronger
and stronger as more well-behaved operations are registered.
The following Isabelle theory fragment gives a flavor of the
envisioned functionality from the user’s point of view:
codatatype

Stream A = SCons (head: A) (tail: Stream A)

corec (well_behaved)

⊕ : Stream → Stream → Stream
xs ⊕ ys = SCons (head xs + head ys) (tail xs ⊕ tail ys)

corec (well_behaved)

⊗ : Stream → Stream → Stream
xs ⊗ ys = SCons (head xs × head ys)
((xs ⊗ tail ys) ⊕ (tail xs ⊗ ys))

lemma ⊕_commute: xs ⊕ ys = ys ⊕ xs
by (coinduction arbitrary: xs ys rule:

stream.coinduct) auto

lemma ⊗_commute: xs ⊗ ys = ys ⊗ xs
proof (coinduction arbitrary: xs ys rule: stream.coinduct_upto)
case Eq_stream
thus ?case unfolding tail_⊗
by (subst ⊕_commute) (auto intro: stream.cl_⊕)
qed

6.

Related Work

There is a lot of relevant work, concerning both the metatheory and
applications in proof assistants and similar systems. We referenced
some of the most closely related work in the earlier sections. Here
is an attempt at a more systematic overview.
Category Theory. The notions of corecursion and coinduction
up-to started with process algebra [44, 47] before they were recast in the abstract language of category theory [8, 22, 26, 28, 38,
43, 50]. Our approach owes a lot to this theoretical work, and indeed formalizes some state-of-the-art category theoretical results
on corecursion and coinduction up-to [38, 43]. Besides adapting
existing results to higher-order logic within an incremental corecursor cycle, we have also extended the state of the art with a sound
mechanism for mixing recursion with corecursion up-to.
Category theory provides an impressive body of abstract results
that can be applied to solve concrete problems elegantly. Proof
assistants have a lot to benefit from category theory, as we hope
to have demonstrated with this paper. There has been prior work
on integrating coinduction up-to techniques from category theory

1. Parse the specification of f and synthesize arguments to the
current, most powerful corecursor.
2. Define f in terms of the corecursor.
3. Derive the original specification from the corecursor theorems.
Passing the well_behaved option to corec will additionally invoke
the following procedure (cf. Example 9):

10

2015/1/23

into these tools. Hensel and Jacobs [20] illustrated the categorical approach to (co)datatypes in PVS via axiomatic declarations
of various flavors of trees with (co)recursors and proof principles.
Popescu and Gunter proposed incremental coinduction for a deeply
embedded proof system in Isabelle/HOL [40]. Hur et al. [25] extended Winskel’s [53] and Moss’s [39] parameterized coinduction
and studied applications to Agda, Coq, and Isabelle/HOL. Endrullis
et al. [19] developed a method to perform up-to coinduction in Coq
adapting insight from behavioral logic [42]. To our knowledge, no
prior work has realized corecursion up-to in a proof assistant.

Clock variables and sized types require an extension to the type
system and burden the types. These general contracts must be specified by the user and complicate the up-to corecursion principle; the
arithmetic that ensures that contracts fit together would have to be
captured in the principle, giving rise to new proof obligations. In
contrast, well-behaved functions can be freely combined. This is
the main reason why we can claim it is a “sweet spot.”
There is a prospect of embedding our lighter approach into such
heavier but more precise frameworks. Our well-behaved operators
possibly form the maximal class of context functions requiring no
annotations (in general), amounting to a lightweight subsystem of
Krishnaswami and Benton’s type system [30].

Ordered Structures and Convergence. A number of approaches
to define functions on infinite types are based on domain theory, or
more generally on ordered structures and notions of convergence,
including Matthews [37], Di Gianantonio and Miculan [17], Huffman [23], and Lochbihler and Hölzl [36]. These are not directly
comparable to our work because they do not guarantee productivity or otherwise offer total programming. They also force the user
to switch to a different, richer universe of domains or to define ordered structures and perform continuity proofs (although Matthews
shows that this process can be partly automated).
Strictly speaking, our approach does not guarantee productivity
either. This is an inherent limitation of the semantic (shallow embedded) approach in HOL systems, which do not specify a computational model (unlike Agda and Coq). Productivity can be argued
informally by inspecting the characteristic corecursion equations.

7.

Conclusion

We presented a formalized framework for deriving rich corecursors
that can be used to define total functions producing codatatypes.
The corecursors gain in expressiveness with each new corecursive
function definition that satisfies a semantic criterion. They constitute a significant improvement over the state of the art in the world
of proof assistants based on higher-order logic, including HOL4,
HOL Light, Isabelle/HOL, and PVS. Trustworthiness is attained at
the cost of elaborate constructions. Coinduction being somewhat
counterintuitive, we argue that these safeguards are well worth the
effort. As future work, we want to transform our prototype tool into
a solid implementation inside Isabelle/HOL.
Although we emphasized the foundational nature of the framework, many of the ideas equally apply to systems with built-in codatatypes and corecursion. One could imagine extending the productivity check of Coq to allow corecursion under well-behaved
operations, linking a syntactic criterion to a semantic property, as
a lightweight alternative to clock variables and sized types. The
emerging infrastructure for parametricity in Coq [11, 27] would
likely be a useful building block.

Syntactic Criteria. Proof assistants based on type theory include
checkers for termination of recursion functions and productivity
of corecursive functions. These checkers are part of the system’s
trusted code base; bugs can lead to inconsistencies, as we saw for
Agda [48] and Coq [16].1 For users, such syntactic criteria are also
inflexible; for example, Coq allows more than one constructor to
appear as guards but is otherwise limited to primitive corecursion.
To the best of our knowledge, the only deployed system that explicitly supports mixed recursive–corecursive definitions is Dafny.
Leino and Moskal’s paper [32] triggered our interest in the topic.
Unfortunately, the paper is not entirely clear about the supported
fragment. A naive reading suggests that the inconsistent nasty example from Section 2.3 is allowed, as was the case with earlier
versions of Dafny. Newer versions reject not only nasty but also
the legitimate cat function from the same subsection.

Acknowledgment. Tobias Nipkow made this work possible. Stefan Milius guided us through his highly relevant work on abstract
GSOS rules. Andreas Abel and Rustan Leino discussed their tools
and shared their paper drafts and examples with us. Mark Summerfield suggested many textual improvements. Reviewers provided
useful comments and indicated related work. Blanchette was supported by the Deutsche Forschungsgemeinschaft (DFG) project
Hardening the Hammer (grant Ni 491/14-1). Popescu was supported by the DFG project Security Type Systems and Deduction
(grant Ni 491/13-2) as part of the program Reliably Secure Software Systems (RS3 , priority program 1496). Traytel was supported
by the DFG program Program and Model Analysis (PUMA, doctorate program 1480). The authors are listed alphabetically.

Type Systems. A more flexible alternative to syntactic criteria
is to have users annotate the functions’ types with information
that controls termination and productivity. Approaches in these
category include fair reactive programming [14, 18, 30], clock
variables [7, 15], and sized types [3]. Size types are implemented in
MiniAgda [4] and in newer versions of Agda, in conjunction with
a destructor-oriented (copattern) syntax for corecursion [5]. These
approaches, often featuring a blend of type systems and notions of
convergence, achieve a higher modularity and trustworthiness, by
moving away from purely syntactic criteria and toward semantic
properties. By carefully tracking sizes and timers, they allow for
more general contexts than our well-behavedness criterion. Our
approach captures a 1–1 contract: A well-behaved function can
destroy one constructor to produce one. A function f that would,
map the stream a1 , a2 , . . . to a1 , a1 , a2 , a2 , . . . would have a 1–
2 contract. And a function g mapping a1 , a2 , a3 , a4 , . . . to a1 +
a2 , a3 + a4 , . . . would require a 2–1 contract. The composition g ◦ f
would yield a 1–1 contract and could in principle appear in a
corecursive call context, but our framework does not allow it.

References
[1] M. Abbott, T. Altenkirch, and N. Ghani. Containers: Constructing
strictly positive types. Theor. Comput. Sci., 342(1):3–27, 2005.
[2] A. Abel. Re: [Coq-Club] Propositional extensionality is inconsistent
in Coq. Archived at https://sympa.inria.fr/sympa/arc/
coq-club/2013-12/msg00147.html.
[3] A. Abel. Termination checking with types. RAIRO—Theor. Inf.
Appl., 38(4):277–319, 2004.
[4] A. Abel. MiniAgda: Integrating sized and dependent types. In
A. Bove, E. Komendantskaya, and M. Niqui, eds., PAR 2010, vol. 43
of EPTCS, pp. 14–28, 2010.
[5] A. Abel and B. Pientka. Wellfounded recursion with copatterns: A
unified approach to termination and productivity. In G. Morrisett and
T. Uustalu, eds., ICFP ’13, pp. 185–196. ACM, 2013.
[6] A. Abel, B. Pientka, D. Thibodeau, and A. Setzer. Copatterns:
Programming infinite structures by observations. In R. Giacobazzi
and R. Cousot, eds., POPL 2013, pp. 27–38, 2013.

1 In

all fairness, we should mention that critical bugs were also found in the
primitive definitional mechanism of our proof assistant of choice, Isabelle
[31]. Our point is not that brand B is superior to brand A, but rather that it
is generally desirable to minimize the amount of trusted code.

11

2015/1/23

[7] R. Atkey and C. McBride. Productive coprogramming with guarded
recursion. In G. Morrisett and T. Uustalu, eds., ICFP ’13,
pp. 197–208. ACM, 2013.

[29] A. Krauss. Partial recursive functions in higher-order logic. In
U. Furbach and N. Shankar, eds., IJCAR 2006, vol. 4130 of LNCS,
pp. 589–603. Springer, 2006.
[30] N. R. Krishnaswami and N. Benton. Ultrametric semantics of
reactive programs. In LICS 2011, pp. 257–266. IEEE, 2011.
[31] O. Kunčar. Correctness of Isabelle’s cyclicity
checker—Implementability of overloading in proof assistants. In
X. Leroy and A. Tiu, eds., CPP 2015, pp. 85–94. ACM, 2015.
[32] K. R. M. Leino and M. Moskal. Co-induction simply—automatic
co-inductive proofs in a program verifier. In C. B. Jones,
P. Pihlajasaari, and J. Sun, eds., FM 2014, vol. 8442 of LNCS,
pp. 382–398. Springer, 2014.

[8] F. Bartels. Generalised coinduction. Math. Struct. Comp. Sci.,
13(2):321–348, 2003.
[9] F. Bartels. On Generalised Coinduction and Probabilistic
Specification Formats: Distributive Laws in Coalgebraic Modelling.
Ph.D. thesis, Vrije Universiteit Amsterdam, 2004.
[10] N. Benton. The proof assistant as an integrated development
environment. In C.-c. Shan, ed., APLAS 2013, vol. 8301 of LNCS,
pp. 307–314. Springer, 2013.
[11] J.-P. Bernardy, P. Jansson, and R. Paterson. Proofs for free:
Parametricity for dependent types. J. Funct. Program.,
22(2):107–152, 2012.

[33] X. Leroy. A formally verified compiler back-end. J. Autom. Reas.,
43(4):363–446, 2009.
[34] A. Lochbihler. Verifying a compiler for Java threads. In A. D.
Gordon, ed., ESOP 2010, vol. 6012 of LNCS, pp. 427–447. Springer,
2010.
[35] A. Lochbihler. Making the Java memory model safe. ACM Trans.
Program. Lang. Syst., 35(4):12:1–65, 2014.

[12] J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu, and
D. Traytel. Truly modular (co)datatypes for Isabelle/HOL. In
G. Klein and R. Gamboa, eds., ITP 2014, vol. 8558 of LNCS,
pp. 93–110. Springer, 2014.
[13] J. C. Blanchette, A. Popescu, and D. Traytel. Formal development
associated with this paper. https://github.com/dtraytel/fouco,
2014.

[36] A. Lochbihler and J. Hölzl. Recursive functions on lazy lists via
domains and topologies. In G. Klein and R. Gamboa, eds., ITP 2014,
vol. 8558 of LNCS, pp. 341–357. Springer, 2014.

[14] A. Cave, F. Ferreira, P. Panangaden, and B. Pientka. Fair reactive
programming. In S. Jagannathan and P. Sewell, eds., POPL ’14,
pp. 361–372. ACM, 2014.

[37] J. Matthews. Recursive function definition over coinductive types. In
Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, eds.,
TPHOLs ’99, vol. 1690 of LNCS, pp. 73–90. Springer, 1999.
[38] S. Milius, L. S. Moss, and D. Schwencke. Abstract GSOS rules and a
modular treatment of recursive definitions. Log. Meth. Comput. Sci.,
9(3), 2013.
[39] L. S. Moss. Parametric corecursion. Theor. Comput. Sci.,
260(1-2):139–163, 2001.
[40] A. Popescu and E. L. Gunter. Incremental pattern-based coinduction
for process algebra and its Isabelle formalization. In C.-H. L. Ong,
ed., FoSSaCS 2010, vol. 6014 of LNCS, pp. 109–127. Springer, 2010.
[41] J. C. Reynolds. Types, abstraction and parametric polymorphism. In
IFIP ’83, pp. 513–523, 1983.
[42] G. Rosu and D. Lucanu. Circular coinduction—A proof theoretical
foundation. In A. Kurz, M. Lenisa, and A. Tarlecki, eds., CALCO
2009, vol. 5728 of LNCS, pp. 127–144. Springer, 2009.
[43] J. Rot, M. M. Bonsangue, and J. J. M. M. Rutten. Coalgebraic
bisimulation-up-to. In P. van Emde Boas, F. C. A. Groen, G. F.
Italiano, J. R. Nawrocki, and H. Sack, eds., SOFSEM 2013, vol. 7741
of LNCS, pp. 369–381. Springer, 2013.

[15] R. Clouston, A. Bizjak, H. B. Grathwohl, , and L. Birkedal.
Programming and reasoning with guarded recursion for coinductive
types. In A. Pitts, ed., FoSSaCS 2015, LNCS. Springer, 2015.
[16] M. Dénès. [Coq-Club] Propositional extensionality is inconsistent in
Coq. Archived at https://sympa.inria.fr/sympa/arc/
coq-club/2013-12/msg00119.html.
[17] P. Di Gianantonio and M. Miculan. A unifying approach to recursive
and co-recursive definitions. In H. Geuvers and F. Wiedijk, eds.,
TYPES 2002, vol. 2646 of LNCS, pp. 148–161. Springer, 2003.
[18] C. Elliott and P. Hudak. Functional reactive animation. In S. L. P.
Jones, M. Tofte, and A. M. Berman, eds., ICFP ’97, pp. 263–273.
ACM, 1997.
[19] J. Endrullis, D. Hendriks, and M. Bodin. Circular coinduction in Coq
using bisimulation-up-to techniques. In S. Blazy, C. Paulin-Mohring,
and D. Pichardie, eds., ITP 2013, vol. 7998 of LNCS, pp. 354–369.
Springer, 2013.
[20] U. Hensel and B. Jacobs. Proof principles for datatypes with iterated
recursion. In E. Moggi and G. Rosolini, eds., CTCS ’97, vol. 1290 of
LNCS, pp. 220–241. Springer, 1997.

[44] J. J. M. M. Rutten. Processes as terms: Non-well-founded models for
bisimulation. Math. Struct. Comp. Sci., 2(3):257–275, 1992.
[45] J. J. M. M. Rutten. Universal coalgebra: A theory of systems. Theor.
Comput. Sci., 249:3–80, 2000.
[46] J. J. M. M. Rutten. A coinductive calculus of streams. Math. Struct.
Comp. Sci., 15(1):93–147, 2005.
[47] D. Sangiorgi. On the bisimulation proof method. Math. Struct.
Comp. Sci., 8(5):447–479, 1998.
[48] D. Traytel. [Agda] Agda’s copatterns incompatible with initial
algebras. Archived at https:
//lists.chalmers.se/pipermail/agda/2014/006759.html.
[49] D. Traytel, A. Popescu, and J. C. Blanchette. Foundational,
compositional (co)datatypes for higher-order logic—Category theory
applied to theorem proving. In LICS 2012, pp. 596–605. IEEE, 2012.

[21] R. Hinze. Concrete stream calculus—An extended study. J. Funct.
Program., 20:463–535, 2010.
[22] R. Hinze and D. W. H. James. Proving the unique fixed-point
principle correct—An adventure with category theory. In ICFP,
pp. 359–371, 2011. Extended version available at http://www.cs.
ox.ac.uk/people/daniel.james/unique/unique-tech.pdf.
[23] B. Huffman. A purely definitional universal domain. In S. Berghofer,
T. Nipkow, C. Urban, and M. Wenzel, eds., TPHOLs 2009, vol. 5674
of LNCS, pp. 260–275. Springer, 2009.
[24] B. Huffman and O. Kunčar. Lifting and Transfer: A modular design
for quotients in Isabelle/HOL. In G. Gonthier and M. Norrish, eds.,
CPP 2013, vol. 8307 of LNCS, pp. 131–146. Springer, 2013.
[25] C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The power of
parameterization in coinductive proof. In R. Giacobazzi and
R. Cousot, eds., POPL ’13, pp. 193–206. ACM, 2013.

[27] C. Keller and M. Lasson. Parametricity in an impredicative sort. In
P. Cégielski and A. Durand, eds., CSL 2012, vol. 16 of LIPIcs,
pp. 381–395. Schloss Dagstuhl, 2012.

[50] D. Turi and G. Plotkin. Towards a mathematical operational
semantics. In LICS 1997, pp. 280–291. IEEE, 1997.
[51] D. A. Turner. Elementary strong functional programming. In P. H.
Hartel and M. J. Plasmeijer, eds., FPLE ’95, vol. 1022 of LNCS,
pp. 1–13. Springer, 1995.
[52] P. Wadler. Theorems for free! In FPCA ’89, pp. 347–359. ACM,
1989.

[28] B. Klin. Bialgebras for structural operational semantics: An
introduction. Theor. Comput. Sci., 412(38):5043–5069, 2011.

[53] G. Winskel. A note on model checking the modal ν-calculus. Theor.
Comput. Sci., 83(1):157–167, 1991.

[26] B. Jacobs. Distributive laws for the coinductive solution of recursive
equations. Inf. Comput., 204(4):561–587, 2006.

12

2015/1/23

