Contextual modal type theory A Nanevski, F Pfenning, B Pientka ACM Transactions on Computational Logic 9 (3), 1-49, 2008 | 363 | 2008 |

Copatterns: programming infinite structures by observations A Abel, B Pientka, D Thibodeau, A Setzer ACM SIGPLAN Notices 48 (1), 27-38, 2013 | 182 | 2013 |

Beluga: A framework for programming and reasoning with deductive systems (system description) B Pientka, J Dunfield Automated Reasoning: 5th International Joint Conference, IJCAR 2010 …, 2010 | 175 | 2010 |

A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions B Pientka ACM SIGPLAN Notices 43 (1), 371-382, 2008 | 163 | 2008 |

Fair reactive programming A Cave, F Ferreira, P Panangaden, B Pientka Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 114* | 2014 |

Wellfounded recursion with copatterns: A unified approach to termination and productivity AM Abel, B Pientka ACM SIGPLAN Notices 48 (9), 185-196, 2013 | 109 | 2013 |

Programming with proofs and explicit contexts B Pientka, J Dunfield Proceedings of the 10th international ACM SIGPLAN conference on Principles …, 2008 | 105 | 2008 |

Programming with binders and indexed data-types A Cave, B Pientka Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2012 | 69 | 2012 |

Well-founded recursion with copatterns and sized types A Abel, B Pientka Journal of Functional Programming 26, e2, 2016 | 65 | 2016 |

Higher-order dynamic pattern unification for dependent types and records A Abel, B Pientka Typed Lambda Calculi and Applications: 10th International Conference, TLCA …, 2011 | 57 | 2011 |

POPLMark reloaded: Mechanizing proofs by logical relations A Abel, G Allais, A Hameer, B Pientka, A Momigliano, S Schäfer, K Stark Journal of Functional Programming 29, e19, 2019 | 53* | 2019 |

Inductive beluga: Programming proofs B Pientka, A Cave Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 50 | 2015 |

Optimizing higher-order pattern unification B Pientka, F Pfenning International Conference on Automated Deduction, 473-487, 2003 | 44 | 2003 |

The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2—a survey AP Felty, A Momigliano, B Pientka Journal of Automated Reasoning 55, 307-372, 2015 | 43 | 2015 |

Tabled higher-order logic programming B Pientka Carnegie Mellon University, 2003 | 39 | 2003 |

Beluga: Programming with dependent types, contextual data, and contexts B Pientka International Symposium on Functional and Logic Programming, 1-12, 2010 | 37 | 2010 |

First-class substitutions in contextual type theory A Cave, B Pientka Proceedings of the Eighth ACM SIGPLAN international workshop on Logical …, 2013 | 33 | 2013 |

Well-founded recursion over contextual objects B Pientka, A Abel 13th International Conference on Typed Lambda Calculi and Applications (TLCA …, 2015 | 31* | 2015 |

An insider’s look at LF type reconstruction: Everything you (n) ever wanted to know B Pientka | 30 | 2010 |

Mechanizing proofs with logical relations–Kripke-style A Cave, B Pientka Mathematical structures in computer science 28 (9), 1606-1638, 2018 | 27* | 2018 |