| A Brief Overview of Agda-A Functional Language with Dependent Types. A Bove, P Dybjer, U Norell TPHOLs 5674, 73-78, 2009 | 361 | 2009 |
| Dependent types at work A Bove, P Dybjer Language Engineering and Rigorous Software Development: International LerNet …, 2009 | 179* | 2009 |
| Modelling general recursion in type theory A Bove, V Capretta Mathematical Structures in Computer Science 15 (4), 671-708, 2005 | 97 | 2005 |
| Nested general recursion and partiality in type theory A Bove, V Capretta Theorem Proving in Higher Order Logics: 14th International Conference …, 2001 | 66 | 2001 |
| 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 |
| General recursion in type theory A Bove Lecture notes in computer science, 39-58, 2003 | 39 | 2003 |
| Partiality and recursion in interactive theorem provers–an overview A Bove, A Krauss, M Sozeau Mathematical Structures in Computer Science 26 (1), 38-88, 2016 | 32 | 2016 |
| Simple general recursion in type theory A Bove Nord. J. Comput. 8 (1), 22-42, 2001 | 28 | 2001 |
| Alpha-structural induction and recursion for the lambda calculus in constructive type theory E Copello, Á Tasistro, N Szasz, A Bove, M Fernández Electronic Notes in Theoretical Computer Science 323, 109-124, 2016 | 17 | 2016 |
| Computation by prophecy A Bove, V Capretta Typed Lambda Calculi and Applications: 8th International Conference, TLCA …, 2007 | 17 | 2007 |
| A confluent calculus of macro expansion and evaluation A Bove, L Arbilla Proceedings of the 1992 ACM Conference on LISP and Functional Programming …, 1992 | 17 | 1992 |
| Programming in Martin-Löf type theory: Unification-A non-trivial example A Bove Licentiate thesis, Department of Computer Science, Chalmers University of …, 1999 | 14* | 1999 |
| Recursive functions with higher order domains A Bove, V Capretta Typed Lambda Calculi and Applications: 7th International Conference, TLCA …, 2005 | 12 | 2005 |
| Formalising bitonic sort in type theory A Bove, T Coquand Types for Proofs and Programs: International Workshop, TYPES 2004, Jouy-en …, 2006 | 10 | 2006 |
| Another look at function domains A Bove Electronic Notes in Theoretical Computer Science 249, 61-74, 2009 | 9 | 2009 |
| A type of partial recursive functions A Bove, V Capretta Lecture Notes in Computer Science 5170, 102-117, 2008 | 8 | 2008 |
| Combining interactive and automatic reasoning in first order theories of functional programs A Bove, P Dybjer, A Sicard-Ramírez Foundations of Software Science and Computational Structures: 15th …, 2012 | 7 | 2012 |
| Language Engineering and Rigorous Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24-March 1, 2008, Revised, Selected Papers A Bove, LS Barbosa, A Pardo, JS Pinto Springer Science & Business Media, 2009 | 6 | 2009 |
| Embedding a logical theory of constructions in agda A Bove, P Dybjer, A Sicard-Ramírez Proceedings of the 3rd workshop on Programming languages meets program …, 2009 | 6 | 2009 |
| Language engineering and rigorous software development. chapter Dependent Types at Work A Bove, P Dybjer Springer-Verlag, Berlin, Heidelberg, 2009 | 5 | 2009 |
Peter DybjerProfessor of Computer Science, Chalmers UniversityVerified email at chalmers.se
