| Contextual modal type theory A Nanevski, F Pfenning, B Pientka ACM Transactions on Computational Logic 9 (3), 1-49, 2008 | 340 | 2008 |
| Copatterns: Programming infinite structures by observations A Abel, B Pientka, D Thibodeau, A Setzer ACM SIGPLAN Notices 48 (1), 27-38, 2013 | 170 | 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 | 165 | 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 | 99 | 2008 |
| Fair reactive programming A Cave, F Ferreira, P Panangaden, B Pientka Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 97* | 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 | 45 | 2015 |
| 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 | 42* | 2019 |
| Optimizing higher-order pattern unification B Pientka, F Pfenning CADE, 473-487, 2003 | 42 | 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 | 39 | 2015 |
| Tabled higher-order logic programming B Pientka Carnegie Mellon University, 2003 | 37 | 2003 |
| Beluga: Programming with dependent types, contextual data, and contexts B Pientka Functional and Logic Programming: 10th International Symposium, FLOPS 2010 …, 2010 | 35 | 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 | 30 | 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 |
