| Universes for generic programs and proofs in dependent type theory M Benke, P Dybjer, P Jansson Nord. J. Comput. 10 (4), 265-289, 2003 | 102 | 2003 |
| Verifying Haskell programs using constructive type theory A Abel, M Benke, A Bove, J Hughes, U Norell Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, 62-73, 2005 | 57 | 2005 |
| A tool for automated theorem proving in Agda F Lindblad, M Benke Types for Proofs and Programs, 154-169, 2006 | 41 | 2006 |
| Efficient type reconstruction in the presence of inheritance M Benke Mathematical Foundations of Computer Science 1993: 18th International …, 1993 | 37 | 1993 |
| Some complexity bounds for subtype inequalities M Benke Institute of Informatics, Warsaw University, 1995 | 10 | 1995 |
| Alonzo - a compiler for Agda M Benke Talk at Agda Implementors Meeting, 2007 | 9 | 2007 |
| Some complexity bounds for subtype inequalities M Benke Theoretical Computer Science 212 (1-2), 3-27, 1999 | 7 | 1999 |
| Complexity of type reconstruction in programming languages with subtyping M Benke Rozprawa doktorska. Uniwersytet Warszawski, Wydział Matematyki, Informatyki …, 1997 | 6 | 1997 |
| Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic M Benke, A Schubert, D Walukiewicz-Chrzaszcz 1st International Conference on Formal Structures for Computation and …, 2016 | 2 | 2016 |
| Predicative polymorphic subtyping M Benke International Symposium on Mathematical Foundations of Computer Science, 326-335, 1998 | 2 | 1998 |
| Strategies for interactive proof and program development in Martin-Löf type theory M Benke proceedings of 4th International Workshop on Strategies in Automated Deduction, 2001 | 1 | 2001 |
| Some tools for computer-assisted theorem proving in Martin-Löf type theory M Benke TPHOLs—Supplemental Proceedings. University of Edinburgh, 2001 | 1 | 2001 |
| An algebraic characterization of typability in ML with subtyping M Benke International Conference on Foundations of Software Science and Computation …, 1999 | 1 | 1999 |
| A logical approach to complexity bounds for subtype inequalities M Benke Gödel'96: Logical foundations of mathematics, computer science and physics …, 1996 | 1 | 1996 |
| A verified IFOL typechecker M Benke, J Chrzaszcz, A Schubert, M Zielenkiewicz | | 2015 |
| Lucretia-intersection type polymorphism for scripting languages M Benke, V Bono, A Schubert arXiv preprint arXiv:1503.04918, 2015 | | 2015 |
| Specifying Functional Programs with Intuitionistic First Order Logic. M Benke CS&P, 57-63, 2015 | | 2015 |
| LIPIcs, Volume 38, TLCA'15, Complete Volume T Altenkirch 13th International Conference on Typed Lambda Calculi and Applications (TLCA …, 2015 | | 2015 |
| LIPIcs, Volume 38, TLCA'15, Complete Volume T Altenkirch 13th International Conference on Typed Lambda Calculi and Applications (TLCA …, 2015 | | 2015 |
| A verified IFOL typechecker—interim report M Benke, J Chrzaszcz, A Schubert Technical report, Institute of Informatics, University of Warsaw, 2014 | | 2014 |
Patrik JanssonProfessor of Computer Science, Chalmers University of TechnologyVerified email at chalmers.se
