Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Wed 21 Sep 2016 11:00 - 11:25 at Noh Theater - Session 9 Chair(s): Sam Lindley

Indexed data types allow us to specify and verify many interesting invariants about finite data in a general purpose programming language. In this paper we investigate the dual idea: indexed codata types, which allow us to describe data-dependencies about infinite data structures. Unlike finite data which is defined by constructors, we define infinite data by observations. Dual to pattern matching on indexed data which may refine the type indices, we define copattern matching on indexed codata where type indices guard observations we can make.

Our key technical contributions are three-fold: first, we extend Levy's call-by-push value language with support for indexed (co)data and deep (co)pattern matching; second, we provide a clean foundation for dependent (co)pattern matching using equality constraints; third, we describe a small-step semantics using a continuation-based abstract machine, define coverage for indexed (co)patterns, and prove type safety. This is an important step towards building a foundation where (co)data type definitions and dependent types can coexist.

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

10:35 - 12:15
Session 9Research Papers at Noh Theater
Chair(s): Sam Lindley University of Edinburgh, UK
10:35
25m
Talk
Ghostbuster: A Tool for Simplifying and Converting GADTs
Research Papers
Trevor L. McDonell Indiana University, USA, Timothy A. K. Zakian Oxford University, UK, Matteo Cimini Indiana University, USA, Ryan R. Newton Indiana University, USA
DOI
11:00
25m
Talk
Indexed Codata Types
Research Papers
David Thibodeau McGill University, Canada, Andrew Cave McGill University, Canada, Brigitte Pientka McGill University, Canada
DOI
11:25
25m
Talk
Disjoint Intersection Types
Research Papers
Bruno C. d. S. Oliveira University of Hong Kong, China, Zhiyuan Shi University of Hong Kong, China, João Alpuim University of Hong Kong, China
DOI
11:50
25m
Talk
Set-Theoretic Types for Polymorphic Variants
Research Papers
Giuseppe Castagna Paris Diderot University & CNRS, Tommaso Petrucciani University of Genoa, France, Kim Nguyễn University of Paris-Sud, France
DOI