| Contextual modal type theory A Nanevski, F Pfenning, B Pientka ACM Transactions on Computational Logic 9 (3), 1-49, 2008 | 369 | 2008 |
| Copatterns: programming infinite structures by observations A Abel, B Pientka, D Thibodeau, A Setzer ACM SIGPLAN Notices 48 (1), 27-38, 2013 | 183 | 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 | 177 | 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 | 164 | 2008 |
| Fair reactive programming A Cave, F Ferreira, P Panangaden, B Pientka Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 115* | 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 | 58 | 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 | 55* | 2019 |
| Inductive beluga: Programming proofs B Pientka, A Cave Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 51 | 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 | 34 | 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 | 31 | 2010 |
| Mechanizing proofs with logical relations–Kripke-style A Cave, B Pientka Mathematical structures in computer science 28 (9), 1606-1638, 2018 | 28* | 2018 |
