Search

• < Previous
• 1
• Next >

---

Refining Inductive Types

Robert Atkey ; Patricia Johann ; Neil Ghani.

Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists&nbsp;[&hellip;]

---

Representations of Stream Processors Using Nested Fixed Points

Neil Ghani ; Peter Hancock ; Dirk Pattinson.

We define representations of continuous functions on infinite streams of discrete values, both in the case of discrete-valued functions, and in the case of stream-valued functions. We define also an operation on the representations of two continuous functions between streams that yields a&nbsp;[&hellip;]

---

Generic Fibrational Induction

Neil Ghani ; Patricia Johann ; Clement Fumex.

This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs' elegant algebraic formulation of induction for&nbsp;[&hellip;]

---

Indexed Induction and Coinduction, Fibrationally

Neil Ghani ; Patricia Johann ; Clement Fumex.

This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we present a dual to the sound induction rule for inductive types that we developed previously. That is, we present a sound&nbsp;[&hellip;]

---

Positive Inductive-Recursive Definitions

Neil Ghani ; Fredrik Nordvall Forsberg ; Lorenzo Malatesta.

A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within&nbsp;[&hellip;]

---