Programming with binders and indexed data-types. - Andrew Cave; Brigitte Pientka (POPL, 2012)

First-class substitutions in contextual type theory. - Andrew Cave; Brigitte Pientka (LFMTP, 2013)

Fair reactive programming. - Andrew Cave; Francisco Ferreira 001; Prakash Panangaden; Brigitte Pientka (POPL, 2014)

Inductive Beluga: Programming Proofs. - Brigitte Pientka; Andrew Cave (CADE, 2015)

A Case Study on Logical Relations using Contextual Types. - Andrew Cave; Brigitte Pientka (LFMTP, 2015)

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

Mechanizing Proofs about Mendler-style Recursion. - Rohan Jacob-Rao; Andrew Cave; Brigitte Pientka (LFMTP, 2016)

Mechanizing proofs with logical relations - Kripke-style. - Andrew Cave; Brigitte Pientka (Math. Struct. Comput. Sci., 2018)