| A brief overview of Agda–a functional language with dependent types A Bove, P Dybjer, U Norell Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009 | 406 | 2009 |
| Dependent types at work A Bove, P Dybjer International LerNet ALFA Summer School on Language Engineering and Rigorous …, 2008 | 161* | 2008 |
| Modelling general recursion in type theory A Bove, V Capretta Mathematical Structures in Computer Science 15 (4), 671-708, 2005 | 106 | 2005 |
| Nested general recursion and partiality in type theory A Bove, V Capretta International Conference on Theorem Proving in Higher Order Logics, 121-125, 2001 | 69 | 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 | 58 | 2005 |
| General recursion in type theory A Bove International Workshop on Types for Proofs and Programs, 39-58, 2002 | 43 | 2002 |
| 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 | 34 | 2016 |
| Simple general recursion in type theory A Bove Nord. J. Comput. 8 (1), 22-42, 2001 | 30 | 2001 |
| Computation by prophecy A Bove, V Capretta International Conference on Typed Lambda Calculi and Applications, 70-83, 2007 | 18 | 2007 |
| 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 |
| 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 International Conference on Typed Lambda Calculi and Applications, 116-130, 2005 | 13 | 2005 |
| Formalising bitonic sort in type theory A Bove, T Coquand International Workshop on Types for Proofs and Programs, 82-97, 2004 | 13 | 2004 |
| 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 International Conference on Theorem Proving in Higher Order Logics, 102-117, 2008 | 9 | 2008 |
| 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 | 8 | 2009 |
| 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 | 7 | 2009 |
| A machine-assisted proof that well typed expressions cannot go wrong A Bove Chalmers University of Technology and Göteborg University, 1998 | 6 | 1998 |
Peter DybjerProfessor of Computer Science, Chalmers University在 chalmers.se 的电子邮件经过验证
