TyDe 2016- Proceedings of the 1st International Workshop on Type-Driven Development

Full Citation in the ACM Digital Library

Generic lookup and update for infinitary inductive-recursive types

APLicative programming with Naperian functors (extended abstract)

Liberating effects with rows and handlers

Programming with monadic CSP-style processes in dependent type theory

Generic partially-static data (extended abstract)

Parameterized extensible effects and session types (extended abstract)

Applications of applicative proof search

Programming assistance for type-directed programming (extended abstract)

choose your own derivative (extended abstract)

An agda formalisation of the transitive closure of block matrices (extended abstract)

Generic Diff3 for algebraic datatypes