Bove, Ana; Dybjer, Peter; Andrés, Sicard-Ramírez: Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012, 7213 pp. 104-118. ISBN/ISSN: 978-3-642-28728-2

Bove, Ana; Komendantskaya, Ekaterina; Niqui, Milad: Proceedings of the workshop on Partiality and Recursion in Interactive Theorem Provers. ISBN/ISSN: 2075-2180

Bove, Ana; Dybjer, Peter; Norell, Ulf: A Brief Overview of Agda - A Functional Language with Dependent Types. Theorem Proving in Higher Order Logics , 5674 (LNCS) pp. 73--78.

Bove, Ana: Another Look at Function Domains. Mathematical Foundations of Programming Semantics, 25th Annual Conference, 249 (ENTCS) pp. 61-74.

Bove, Ana; Dybjer, Peter: Dependent Types at Work. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer Schoo, 5520 (LNCS) pp. 57--99.

Bove, Ana; Dybjer, Peter; Sicard-Ramirez, Andres: Embedding a Logical Theory of Constructions in Agda. Programming Languages meets Program Verification (PLPV) 2009 , (ACM digital library)

Language Engineering and Rigorous Software Development. Ana Bove, Luis Barbosa, Alberto Pardo, Jorge Sousa Pinto [editor(s)].

Bove, Ana; Capretta, Venanzio: A Type of Partial Recursive Functions. Theorem Proving in Higher Order Logics, 21st International Conference TPHOLs 2008, LNCS 5170 pp. 102--117. ISBN/ISSN: 978-3-540-71065-3

Bove, Ana; Capretta, Venanzio: Computation by Prophecy. Typed Lambda Calculus and Applications; Simona Ronchi Della Rocca (Ed.), 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings. (Lecture notes in computer science; 4583 ), pp. 70--83. ISBN/ISSN: 978-3-540-73227-3

Abel, Andreas; Benke, Marcin; Bove, Ana; Hughes, John; Norell, Ulf: Verifying Haskell Programs Using Constructive Type Theory. Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, ISBN/ISSN: 1-59593-071-X

Bove, Ana; Coquand, Thierry: Formalising Bitonic Sort in Type Theory. Types for Proofs and Programs TYPES 2004, LNCS 3839 pp. 82-97.

Bove, Ana; Capretta, Venanzio: Modelling General Recursion in Type Theory. Mathematical Structures in Computer Science, 15 pp. 671--708.

Bove, Ana; Capretta, Venanzio: Recursive Functions with Higher Order Domains. Typed Lambda Calculus and Applications TLCA 2005, (LNCS 3461) pp. 116--130.

Bove, Ana: Formalising Bitonic Sort using Dependent Types. Göteborg : Chalmers University of Technology.

Bove, Ana: General Recursion in Type Theory. Lecture Notes in Computer Science. International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24–28, 2002, 2646 pp. 39-58. ISBN/ISSN: 978-3-540-14031-3

Bove, Ana: General Recursion in Type Theory. Göteborg : Chalmers University of Technology. Diss.

Bove, Ana: Generalised Simultaneous Inductive-Recursive Definitions and their Application to Programming in Type Theory. Göteborg : Chalmers University of Technology.

Bove, Ana: Mutual General Recursion in Type Theory. Göteborg : Chalmers University of Technology.

Bove, Ana; Capretta, Venanzio: Nested General Recursion and Partiality in Type Theory. Theorem Proving in Higher Order Logics, LNCS 2152 pp. 121--135. ISBN/ISSN: 3-540-42525-X

Bove, Ana: Simple General Recursion in Type Theory. Nordic Journal of Computing, 8 pp. 22--42.

Bove, Ana; Severi, Paula: Alpha Conversion in Simply Typed Lambda Calculus. 6th Workshop on Logic, Language, Information and Computation,

Bove, Ana: Programming in Martin-Löf Type Theory: Unification - A non-trivial Example. Göteborg : Chalmers University of Technology.

Bove, Ana: A Machine-assisted Proof that Well Typed Expressions Cannot Go Wrong. Göteborg : Chalmers University of Technology.

Bove, Ana; Tasistro, Alvaro: A Machine-assisted Proof of the Subject Reduction Property for a Small Typed Functional Language. Workshop on Logic, Language, Information and Computation,

Bove, Ana: A Machine-assisted Proof of the Subject Reduction Property for a Small Typed Functional Language. Uruguay : Department of Computer Science, Universidad de la República.

Bove, Ana; Arbilla, Laura: A Confluent Calculus of Macro Expansion and Evaluation. Lisp and Functional Programming ,