Copatterns: programming infinite structures by observations. - Andreas Abel 001; Brigitte Pientka; David Thibodeau 001; Anton Setzer (POPL, 2013)

Unnesting of Copatterns. - Anton Setzer; Andreas Abel 001; Brigitte Pientka; David Thibodeau 001 (RTA-TLCA, 2014)

Indexed codata types. - David Thibodeau 001; Andrew Cave; Brigitte Pientka (ICFP, 2016)

Index-Stratified Types. - Rohan Jacob-Rao; Brigitte Pientka; David Thibodeau 001 (FSCD, 2018)

Index-Stratified Types (Extended Version). - Rohan Jacob-Rao; Brigitte Pientka; David Thibodeau 001 (CoRR, 2018)

A Type Theory for Defining Logics and Proofs. - Brigitte Pientka; David Thibodeau 001; Andreas Abel 001; Francisco Ferreira 001; Rébecca Zucchini (LICS, 2019)

Cocon: Computation in Contextual Type Theory. - Brigitte Pientka; Andreas Abel 001; Francisco Ferreira 001; David Thibodeau 001; Rébecca Zucchini (CoRR, 2019)

A case study in programming coinductive proofs: Howe's method. - Alberto Momigliano; Brigitte Pientka; David Thibodeau 001 (Math. Struct. Comput. Sci., 2019)