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

Copatterns: Programming infinite structures by observations A Abel, B Pientka, D Thibodeau, A Setzer ACM SIGPLAN Notices 48 (1), 27-38, 2013 | 167 | 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 | 164 | 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 | 157 | 2008 |

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

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

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

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

Well-founded recursion with copatterns and sized types A Abel, B Pientka Journal of Functional Programming 26, e2, 2016 | 62 | 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 | 49 | 2011 |

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

Optimizing higher-order pattern unification B Pientka, F Pfenning CADE, 473-487, 2003 | 42 | 2003 |

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 | 37* | 2019 |

Tabled higher-order logic programming B Pientka Carnegie Mellon University, 2003 | 37 | 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 | 35 | 2015 |

Beluga: Programming with dependent types, contextual data, and contexts B Pientka Functional and Logic Programming: 10th International Symposium, FLOPS 2010 …, 2010 | 34 | 2010 |

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

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

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

Reasoning with higher-order abstract syntax and contexts: A comparison A Felty, B Pientka Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010 | 26 | 2010 |