A Confluent Calculus of Macro Expansion and Evaluation. - Ana Bove; Laura Arbilla (LISP and Functional Programming, 1992)

Nested General Recursion and Partiality in Type Theory. - Ana Bove; Venanzio Capretta (TPHOLs, 2001)

Simple General Recursion in Type Theory. - Ana Bove (Nord. J. Comput., 2001)

General Recursion in Type Theory. - Ana Bove (TYPES, 2002)

General Recursion in Type Theory. - Ana Bove (2002)

Formalising Bitonic Sort in Type Theory. - Ana Bove; Thierry Coquand (TYPES, 2004)

Verifying haskell programs using constructive type theory. - Andreas Abel 001; Marcin Benke; Ana Bove; John Hughes 001; Ulf Norell (Haskell, 2005)

Recursive Functions with Higher Order Domains. - Ana Bove; Venanzio Capretta (TLCA, 2005)

Modelling general recursion in type theory. - Ana Bove; Venanzio Capretta (Math. Struct. Comput. Sci., 2005)

Computation by Prophecy. - Ana Bove; Venanzio Capretta (TLCA, 2007)

Dependent Types at Work. - Ana Bove; Peter Dybjer (LerNet ALFA Summer School, 2008)

A Type of Partial Recursive Functions. - Ana Bove; Venanzio Capretta (TPHOLs, 2008)

Embedding a logical theory of constructions in Agda. - Ana Bove; Peter Dybjer; Andrés Sicard-Ramírez (PLPV, 2009)

A Brief Overview of Agda - A Functional Language with Dependent Types. - Ana Bove; Peter Dybjer; Ulf Norell (TPHOLs, 2009)

Another Look at Function Domains. - Ana Bove (MFPS, 2009)

Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. - Ana Bove; Peter Dybjer; Andrés Sicard-Ramírez (FoSSaCS, 2012)

Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory. - Ernesto Copello; Alvaro Tasistro; Nora Szasz; Ana Bove; Maribel Fernández (LSFA, 2015)

Partiality and recursion in interactive theorem provers - an overview. - Ana Bove; Alexander Krauss 001; Matthieu Sozeau (Math. Struct. Comput. Sci., 2016)