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 | 384 | 2009 |

Dependent types at work A Bove, P Dybjer International LerNet ALFA Summer School on Language Engineering and Rigorous …, 2008 | 173* | 2008 |

Modelling general recursion in type theory A Bove, V Capretta Mathematical Structures in Computer Science 15 (4), 671-708, 2005 | 105 | 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 | 68 | 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 | 44 | 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 | 33 | 2016 |

Simple general recursion in type theory A Bove Nord. J. Comput. 8 (1), 22-42, 2001 | 28 | 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 | 11 | 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 |

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 |

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 | 7 | 2009 |

Language engineering and rigorous software development. chapter Dependent Types at Work A Bove, P Dybjer Springer-Verlag, Berlin, Heidelberg, 2009 | 5 | 2009 |