4 results
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 […]
Published on June 19, 2012
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 […]
Published on August 28, 2013
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 […]
Published on June 4, 2012
Patricia Johann ; Enrico Ghiorzi.
This paper considers parametricity and its consequent free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style […]
Published on December 23, 2021